Nuprl Lemma : sub-equality

[T:Type]. ∀[P:T ⟶ ℙ]. ∀[i,u:T].  (i u ∈ {j:T| {j:T| j} supposing ((P u) and (i u ∈ T))


Proof




Definitions occuring in Statement :  uimplies: supposing a uall: [x:A]. B[x] prop: set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: subtype_rel: A ⊆B
Lemmas referenced :  equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis applyEquality hypothesisEquality sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin axiomEquality because_Cache equalityTransitivity equalitySymmetry lemma_by_obid functionEquality cumulativity universeEquality dependent_set_memberEquality setEquality lambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[i,u:T].    (i  =  u)  supposing  ((P  u)  and  (i  =  u))



Date html generated: 2016_05_15-PM-03_38_03
Last ObjectModification: 2015_12_27-PM-01_16_12

Theory : general


Home Index