Nuprl Lemma : dep-isect_wf
∀A:𝕌'. ∀B:A ⟶ 𝕌'. (x:A ⋂ B[x] ∈ 𝕌')
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:\mBbbU{}'. \mforall{}B:A {}\mrightarrow{} \mBbbU{}'. (x:A \mcap{} B[x] \mmember{} \mBbbU{}')
Date html generated:
2016_05_15-PM-02_07_01
Last ObjectModification:
2015_12_27-AM-00_28_07
Theory : dependent!intersection
Home
Index