Nuprl Lemma : subtype_by_equality

[A,B:Type].  ((∀x,y:Base.  ((x y ∈ A)  (x y ∈ B)))  (A ⊆B))


Proof




Definitions occuring in Statement :  subtype_rel: A ⊆B uall: [x:A]. B[x] all: x:A. B[x] implies:  Q base: Base universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q subtype_rel: A ⊆B all: x:A. B[x] squash: T prop: label: ...$L... t guard: {T} true: True
Lemmas referenced :  base_wf member_wf squash_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :lambdaFormation_alt,  Error :lambdaEquality_alt,  Error :universeIsType,  hypothesisEquality sqequalRule Error :functionIsType,  extract_by_obid hypothesis Error :inhabitedIsType,  Error :equalityIsType4,  because_Cache sqequalHypSubstitution dependent_functionElimination thin axiomEquality Error :isect_memberEquality_alt,  isectElimination universeEquality pointwiseFunctionality equalityTransitivity equalitySymmetry independent_functionElimination applyEquality imageElimination natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[A,B:Type].    ((\mforall{}x,y:Base.    ((x  =  y)  {}\mRightarrow{}  (x  =  y)))  {}\mRightarrow{}  (A  \msubseteq{}r  B))



Date html generated: 2019_06_20-PM-00_28_09
Last ObjectModification: 2018_09_29-PM-11_18_30

Theory : subtype_1


Home Index