Nuprl Lemma : int-deq-aux

`∀[a,b:ℤ].  uiff(a = b ∈ ℤ;↑(a =z b))`

Proof

Definitions occuring in Statement :  assert: `↑b` eq_int: `(i =z j)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` implies: `P `` Q` iff: `P `⇐⇒` Q`
Lemmas referenced :  equal-wf-base int_subtype_base iff_weakening_uiff assert_wf eq_int_wf assert_of_eq_int assert_witness uiff_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesisEquality applyEquality sqequalRule because_Cache addLevel productElimination independent_isectElimination independent_functionElimination instantiate cumulativity independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry axiomEquality

Latex:
\mforall{}[a,b:\mBbbZ{}].    uiff(a  =  b;\muparrow{}(a  =\msubz{}  b))

Date html generated: 2019_06_20-PM-00_31_55
Last ObjectModification: 2018_08_24-PM-10_58_43

Theory : equality!deciders

Home Index