MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subggrp Structured version   Unicode version

Theorem subggrp 16076
Description: A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypothesis
Ref Expression
subggrp.h  |-  H  =  ( Gs  S )
Assertion
Ref Expression
subggrp  |-  ( S  e.  (SubGrp `  G
)  ->  H  e.  Grp )

Proof of Theorem subggrp
StepHypRef Expression
1 subggrp.h . 2  |-  H  =  ( Gs  S )
2 eqid 2467 . . . 4  |-  ( Base `  G )  =  (
Base `  G )
32issubg 16073 . . 3  |-  ( S  e.  (SubGrp `  G
)  <->  ( G  e. 
Grp  /\  S  C_  ( Base `  G )  /\  ( Gs  S )  e.  Grp ) )
43simp3bi 1013 . 2  |-  ( S  e.  (SubGrp `  G
)  ->  ( Gs  S
)  e.  Grp )
51, 4syl5eqel 2559 1  |-  ( S  e.  (SubGrp `  G
)  ->  H  e.  Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767    C_ wss 3481   ` cfv 5594  (class class class)co 6295   Basecbs 14507   ↾s cress 14508   Grpcgrp 15925  SubGrpcsubg 16067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fv 5602  df-ov 6298  df-subg 16070
This theorem is referenced by:  subg0  16079  subginv  16080  subg0cl  16081  subginvcl  16082  subgcl  16083  issubg2  16088  issubgrpd  16090  subsubg  16096  resghm  16155  resghm2b  16157  subgga  16210  gasubg  16212  odsubdvds  16464  pgp0  16489  subgpgp  16490  sylow2blem2  16514  slwhash  16517  fislw  16518  subglsm  16564  pj1ghm  16594  subgabl  16717  cycsubgcyg  16776  subgdmdprd  16953  subgdprd  16954  ablfacrplem  16988  pgpfaclem1  17004  pgpfaclem3  17006  ablfaclem3  17010  issubrg2  17320  islss3  17476  mplgrp  17982  zringcyg  18382  zcyg  18387  expghmOLD  18399  cnmsgngrp  18484  psgnghm  18485  scmatghm  18904  m2cpmrngiso  19128  subgtgp  20472  subgngp  21017  reefgim  22712
  Copyright terms: Public domain W3C validator