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

Theorem subgss 15703
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 15702 . 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 3349   ` cfv 5439  (class class class)co 6112   Basecbs 14195   ↾s cress 14196   Grpcgrp 15431  SubGrpcsubg 15696
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 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552
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 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fv 5447  df-ov 6115  df-subg 15699
This theorem is referenced by:  subgbas  15706  subg0  15708  subginv  15709  subgsubcl  15713  subgsub  15714  subgmulgcl  15715  subgmulg  15716  issubg2  15717  issubg4  15721  subsubg  15725  subgint  15726  nsgconj  15735  nsgacs  15738  ssnmz  15744  eqger  15752  eqgid  15754  eqgen  15755  eqgcpbl  15756  lagsubg2  15763  lagsubg  15764  resghm  15784  ghmnsgima  15791  conjsubg  15799  conjsubgen  15800  conjnmz  15801  conjnmzb  15802  gicsubgen  15827  subgga  15839  gasubg  15841  gastacos  15849  orbstafun  15850  cntrsubgnsg  15879  oddvds2  16088  subgpgp  16117  odcau  16124  pgpssslw  16134  sylow2blem1  16140  sylow2blem2  16141  sylow2blem3  16142  slwhash  16144  fislw  16145  sylow2  16146  sylow3lem1  16147  sylow3lem2  16148  sylow3lem3  16149  sylow3lem4  16150  sylow3lem5  16151  sylow3lem6  16152  lsmval  16168  lsmelval  16169  lsmelvali  16170  lsmelvalm  16171  lsmsubg  16174  lsmub1  16176  lsmub2  16177  lsmless1  16179  lsmless2  16180  lsmless12  16181  lsmass  16188  subglsm  16191  lsmmod  16193  cntzrecd  16196  lsmcntz  16197  lsmcntzr  16198  lsmdisj2  16200  subgdisj1  16209  pj1f  16215  pj1id  16217  pj1lid  16219  pj1rid  16220  pj1ghm  16221  subgabl  16341  ablcntzd  16360  lsmcom  16361  dprdff  16518  dprdffOLD  16524  dprdfadd  16532  dprdfaddOLD  16539  dprdres  16547  dprdss  16548  subgdmdprd  16553  dprdcntz2  16558  dmdprdsplit2lem  16566  ablfacrp  16589  ablfac1eu  16596  pgpfac1lem1  16597  pgpfac1lem2  16598  pgpfac1lem3a  16599  pgpfac1lem3  16600  pgpfac1lem4  16601  pgpfac1lem5  16602  pgpfaclem1  16604  pgpfaclem2  16605  pgpfaclem3  16606  ablfaclem3  16610  ablfac2  16612  issubrg2  16907  issubrg3  16915  islss4  17065  mpllsslem  17533  mpllsslemOLD  17535  subgtgp  19698  subgntr  19699  opnsubg  19700  clssubg  19701  clsnsg  19702  cldsubg  19703  divstgpopn  19712  divstgphaus  19715  tgptsmscls  19746  subgnm  20241  subgngp  20243  lssnlm  20303  idomsubgmo  29589
  Copyright terms: Public domain W3C validator