Nuprl Lemma : eq_bool_wf

[p,q:𝔹].  (p =b q ∈ 𝔹)


Proof




Definitions occuring in Statement :  eq_bool: =b q bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T eq_bool: =b q prop: uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a
Lemmas referenced :  bor_wf band_wf assert_wf bnot_wf assert_of_bnot bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality hypothesis productElimination independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  Error :universeIsType

Latex:
\mforall{}[p,q:\mBbbB{}].    (p  =b  q  \mmember{}  \mBbbB{})



Date html generated: 2019_06_20-AM-11_31_11
Last ObjectModification: 2018_09_26-AM-11_24_47

Theory : bool_1


Home Index