Nuprl Lemma : subtype_rel_functionality_wrt_iff

`∀[A,B,C,D:Type].  ({uiff(A ⊆r B;C ⊆r D)}) supposing (B ≡ D and A ≡ C)`

Proof

Definitions occuring in Statement :  ext-eq: `A ≡ B` uiff: `uiff(P;Q)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` guard: `{T}` universe: `Type`
Definitions unfolded in proof :  guard: `{T}` ext-eq: `A ≡ B` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` prop: `ℙ`
Lemmas referenced :  subtype_rel_transitivity subtype_rel_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin independent_pairFormation hypothesis lemma_by_obid isectElimination hypothesisEquality independent_isectElimination axiomEquality independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry because_Cache universeEquality

Latex:
\mforall{}[A,B,C,D:Type].    (\{uiff(A  \msubseteq{}r  B;C  \msubseteq{}r  D)\})  supposing  (B  \mequiv{}  D  and  A  \mequiv{}  C)

Date html generated: 2016_05_13-PM-03_19_08
Last ObjectModification: 2015_12_26-AM-09_07_52

Theory : subtype_0

Home Index