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

Theorem subgss 15671
Description: A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypothesis
Ref Expression
issubg.b  |-  B  =  ( Base `  G
)
Assertion
Ref Expression
subgss  |-  ( S  e.  (SubGrp `  G
)  ->  S  C_  B
)

Proof of Theorem subgss
StepHypRef Expression
1 issubg.b . . 3  |-  B  =  ( Base `  G
)
21issubg 15670 . 2  |-  ( S  e.  (SubGrp `  G
)  <->  ( G  e. 
Grp  /\  S  C_  B  /\  ( Gs  S )  e.  Grp ) )
32simp2bi 1004 1  |-  ( S  e.  (SubGrp `  G
)  ->  S  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756    C_ wss 3321   ` cfv 5411  (class class class)co 6086   Basecbs 14166   ↾s cress 14167   Grpcgrp 15402  SubGrpcsubg 15664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fv 5419  df-ov 6089  df-subg 15667
This theorem is referenced by:  subgbas  15674  subg0  15676  subginv  15677  subgsubcl  15681  subgsub  15682  subgmulgcl  15683  subgmulg  15684  issubg2  15685  issubg4  15689  subsubg  15693  subgint  15694  nsgconj  15703  nsgacs  15706  ssnmz  15712  eqger  15720  eqgid  15722  eqgen  15723  eqgcpbl  15724  lagsubg2  15731  lagsubg  15732  resghm  15752  ghmnsgima  15759  conjsubg  15767  conjsubgen  15768  conjnmz  15769  conjnmzb  15770  gicsubgen  15795  subgga  15807  gasubg  15809  gastacos  15817  orbstafun  15818  cntrsubgnsg  15847  oddvds2  16056  subgpgp  16085  odcau  16092  pgpssslw  16102  sylow2blem1  16108  sylow2blem2  16109  sylow2blem3  16110  slwhash  16112  fislw  16113  sylow2  16114  sylow3lem1  16115  sylow3lem2  16116  sylow3lem3  16117  sylow3lem4  16118  sylow3lem5  16119  sylow3lem6  16120  lsmval  16136  lsmelval  16137  lsmelvali  16138  lsmelvalm  16139  lsmsubg  16142  lsmub1  16144  lsmub2  16145  lsmless1  16147  lsmless2  16148  lsmless12  16149  lsmass  16156  subglsm  16159  lsmmod  16161  cntzrecd  16164  lsmcntz  16165  lsmcntzr  16166  lsmdisj2  16168  subgdisj1  16177  pj1f  16183  pj1id  16185  pj1lid  16187  pj1rid  16188  pj1ghm  16189  subgabl  16309  ablcntzd  16328  lsmcom  16329  dprdff  16482  dprdffOLD  16488  dprdfadd  16496  dprdfaddOLD  16503  dprdres  16511  dprdss  16512  subgdmdprd  16517  dprdcntz2  16522  dmdprdsplit2lem  16530  ablfacrp  16553  ablfac1eu  16560  pgpfac1lem1  16561  pgpfac1lem2  16562  pgpfac1lem3a  16563  pgpfac1lem3  16564  pgpfac1lem4  16565  pgpfac1lem5  16566  pgpfaclem1  16568  pgpfaclem2  16569  pgpfaclem3  16570  ablfaclem3  16574  ablfac2  16576  issubrg2  16861  issubrg3  16869  islss4  17017  mpllsslem  17485  mpllsslemOLD  17487  subgtgp  19645  subgntr  19646  opnsubg  19647  clssubg  19648  clsnsg  19649  cldsubg  19650  divstgpopn  19659  divstgphaus  19662  tgptsmscls  19693  subgnm  20188  subgngp  20190  lssnlm  20250  idomsubgmo  29506
  Copyright terms: Public domain W3C validator