Nuprl Lemma : grp_eq_sym

[g:DMon]. ∀[a,b:|g|].  =b =b a


Proof




Definitions occuring in Statement :  dmon: DMon grp_eq: =b grp_car: |g| bool: 𝔹 uall: [x:A]. B[x] infix_ap: y equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T infix_ap: y dmon: DMon mon: Mon uimplies: supposing a iff: ⇐⇒ Q and: P ∧ Q implies:  Q prop: rev_implies:  Q uiff: uiff(P;Q)
Lemmas referenced :  iff_imp_equal_bool grp_eq_wf equal_wf grp_car_wf assert_of_mon_eq assert_wf iff_wf dmon_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin applyEquality setElimination rename hypothesisEquality hypothesis independent_isectElimination independent_pairFormation lambdaFormation equalitySymmetry addLevel productElimination impliesFunctionality because_Cache sqequalRule isect_memberEquality axiomEquality

Latex:
\mforall{}[g:DMon].  \mforall{}[a,b:|g|].    a  =\msubb{}  b  =  b  =\msubb{}  a



Date html generated: 2016_05_15-PM-00_07_08
Last ObjectModification: 2015_12_26-PM-11_46_58

Theory : groups_1


Home Index