Nuprl Lemma : eq_int-wf-partial2

[x,y:partial(ℤ)].  ((x =z y) ∈ partial(𝔹))


Proof




Definitions occuring in Statement :  partial: partial(T) eq_int: (i =z j) bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uimplies: supposing a
Lemmas referenced :  eq_int-wf-partial subtype_rel_partial base_wf int_subtype_base partial_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality intEquality hypothesis independent_isectElimination sqequalRule because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[x,y:partial(\mBbbZ{})].    ((x  =\msubz{}  y)  \mmember{}  partial(\mBbbB{}))



Date html generated: 2016_05_14-AM-06_10_32
Last ObjectModification: 2015_12_26-AM-11_51_49

Theory : partial_1


Home Index