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 :  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:\mBbbU{}'.  \mforall{}B:A  {}\mrightarrow{}  \mBbbU{}'.    (x:A  \mcap{}  B[x]  \mmember{}  \mBbbU{}')



Date html generated: 2019_06_20-PM-00_35_01
Last ObjectModification: 2019_01_11-PM-03_19_39

Theory : dependent!intersection


Home Index