Nuprl Lemma : dep-isect-wf
∀A:Type. ∀B:A ⟶ Type. (x:A ⋂ B[x] ∈ Type)
Proof
Definitions occuring in Statement :
dep-isect: x:A ⋂ B[x],
so_apply: x[s],
all: ∀x:A. B[x],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
so_apply: x[s]
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
hypothesis,
functionEquality,
cumulativity,
hypothesisEquality,
universeEquality,
dependentIntersectionEquality,
applyEquality
Latex:
\mforall{}A:Type. \mforall{}B:A {}\mrightarrow{} Type. (x:A \mcap{} B[x] \mmember{} Type)
Date html generated:
2016_05_15-PM-02_07_03
Last ObjectModification:
2015_12_27-AM-00_28_08
Theory : dependent!intersection
Home
Index