### Nuprl Lemma : equal_subtype

`∀[A,B:Type]. ∀[a1,a2:A]. ∀[b1,b2:B].  (a1 = a2 ∈ A) ⊆r (b1 = b2 ∈ B) supposing (a1 = a2 ∈ A) `` (b1 = b2 ∈ B)`

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` implies: `P `` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` subtype_rel: `A ⊆r B` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality sqequalHypSubstitution independent_functionElimination thin hypothesis equalityElimination axiomEquality extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule functionEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[a1,a2:A].  \mforall{}[b1,b2:B].    (a1  =  a2)  \msubseteq{}r  (b1  =  b2)  supposing  (a1  =  a2)  {}\mRightarrow{}  (b1  =  b2)

Date html generated: 2017_04_14-AM-07_36_38
Last ObjectModification: 2017_02_27-PM-03_08_47

Theory : subtype_1

Home Index