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

Theorem subgss 16818
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 16817 . 2  |-  ( S  e.  (SubGrp `  G
)  <->  ( G  e. 
Grp  /\  S  C_  B  /\  ( Gs  S )  e.  Grp ) )
32simp2bi 1024 1  |-  ( S  e.  (SubGrp `  G
)  ->  S  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    e. wcel 1887    C_ wss 3404   ` cfv 5582  (class class class)co 6290   Basecbs 15121   ↾s cress 15122   Grpcgrp 16669  SubGrpcsubg 16811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fv 5590  df-ov 6293  df-subg 16814
This theorem is referenced by:  subgbas  16821  subg0  16823  subginv  16824  subgsubcl  16828  subgsub  16829  subgmulgcl  16830  subgmulg  16831  issubg2  16832  issubg4  16836  subsubg  16840  subgint  16841  nsgconj  16850  nsgacs  16853  ssnmz  16859  eqger  16867  eqgid  16869  eqgen  16870  eqgcpbl  16871  lagsubg2  16878  lagsubg  16879  resghm  16899  ghmnsgima  16906  conjsubg  16914  conjsubgen  16915  conjnmz  16916  conjnmzb  16917  gicsubgen  16942  subgga  16954  gasubg  16956  gastacos  16964  orbstafun  16965  cntrsubgnsg  16994  oddvds2  17217  subgpgp  17249  odcau  17256  pgpssslw  17266  sylow2blem1  17272  sylow2blem2  17273  sylow2blem3  17274  slwhash  17276  fislw  17277  sylow2  17278  sylow3lem1  17279  sylow3lem2  17280  sylow3lem3  17281  sylow3lem4  17282  sylow3lem5  17283  sylow3lem6  17284  lsmval  17300  lsmelval  17301  lsmelvali  17302  lsmelvalm  17303  lsmsubg  17306  lsmub1  17308  lsmub2  17309  lsmless1  17311  lsmless2  17312  lsmless12  17313  lsmass  17320  subglsm  17323  lsmmod  17325  cntzrecd  17328  lsmcntz  17329  lsmcntzr  17330  lsmdisj2  17332  subgdisj1  17341  pj1f  17347  pj1id  17349  pj1lid  17351  pj1rid  17352  pj1ghm  17353  subgabl  17476  ablcntzd  17495  lsmcom  17496  dprdff  17645  dprdfadd  17653  dprdres  17661  dprdss  17662  subgdmdprd  17667  dprdcntz2  17671  dmdprdsplit2lem  17678  ablfacrp  17699  ablfac1eu  17706  pgpfac1lem1  17707  pgpfac1lem2  17708  pgpfac1lem3a  17709  pgpfac1lem3  17710  pgpfac1lem4  17711  pgpfac1lem5  17712  pgpfaclem1  17714  pgpfaclem2  17715  pgpfaclem3  17716  ablfaclem3  17720  ablfac2  17722  issubrg2  18028  issubrg3  18036  islss4  18185  mpllsslem  18659  subgtgp  21120  subgntr  21121  opnsubg  21122  clssubg  21123  clsnsg  21124  cldsubg  21125  qustgpopn  21134  qustgphaus  21137  tgptsmscls  21164  subgnm  21641  subgngp  21643  lssnlm  21703  efgh  23490  efabl  23499  efsubm  23500  idomsubgmo  36072
  Copyright terms: Public domain W3C validator