Nuprl Lemma : ocgrp_abdgrp

[g:OGrp]. (g ∈ AbDGrp)


Proof




Definitions occuring in Statement :  ocgrp: OGrp abdgrp: AbDGrp uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B
Lemmas referenced :  ocgrp_subtype_abdgrp ocgrp_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality applyEquality thin lemma_by_obid hypothesis sqequalHypSubstitution sqequalRule axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[g:OGrp].  (g  \mmember{}  AbDGrp)



Date html generated: 2016_05_15-PM-00_13_15
Last ObjectModification: 2015_12_26-PM-11_41_45

Theory : groups_1


Home Index