### Nuprl Lemma : iff_imp_equal_bool

`∀[a,b:𝔹].  a = b supposing ↑a `⇐⇒` ↑b`

Proof

Definitions occuring in Statement :  assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` prop: `ℙ` rev_implies: `P `` Q` false: `False` true: `True` bfalse: `ff` ifthenelse: `if b then t else f fi ` assert: `↑b` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹`
Lemmas referenced :  assert_wf iff_wf bool_wf bfalse_wf btrue_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut hypothesis sqequalRule Error :productIsType,  Error :functionIsType,  Error :universeIsType,  extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  voidElimination natural_numberEquality independent_functionElimination productElimination equalityElimination unionElimination

Latex:
\mforall{}[a,b:\mBbbB{}].    a  =  b  supposing  \muparrow{}a  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}b

Date html generated: 2019_06_20-AM-11_31_25
Last ObjectModification: 2018_09_26-AM-11_16_10

Theory : bool_1

Home Index