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 :
member: t ∈ T,
all: ∀x:A. B[x],
so_apply: x[s]
Rules used in proof :
universeEquality,
hypothesisEquality,
cumulativity,
functionEquality,
hypothesis,
sqequalHypSubstitution,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
dependentIntersectionEquality,
applyEquality
Latex:
\mforall{}A:Type. \mforall{}B:A {}\mrightarrow{} Type. (x:A \mcap{} B[x] \mmember{} Type)
Date html generated:
2019_06_20-PM-00_35_02
Last ObjectModification:
2019_01_09-PM-02_48_08
Theory : dependent!intersection
Home
Index