Nuprl Lemma : subtype_rel_b-union-right

[A,B:Type].  (B ⊆(A ⋃ B))


Proof




Definitions occuring in Statement :  b-union: A ⋃ B subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B b-union: A ⋃ B tunion: x:A.B[x] ifthenelse: if then else fi  bfalse: ff pi2: snd(t)
Lemmas referenced :  ifthenelse_wf bfalse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality sqequalRule imageMemberEquality dependent_pairEquality lemma_by_obid hypothesis hypothesisEquality thin instantiate sqequalHypSubstitution isectElimination universeEquality baseClosed equalityTransitivity equalitySymmetry axiomEquality isect_memberEquality because_Cache

Latex:
\mforall{}[A,B:Type].    (B  \msubseteq{}r  (A  \mcup{}  B))



Date html generated: 2016_05_13-PM-03_57_49
Last ObjectModification: 2016_01_14-PM-07_21_07

Theory : bool_1


Home Index