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

Theorem subgss 16071
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 16070 . 2  |-  ( S  e.  (SubGrp `  G
)  <->  ( G  e. 
Grp  /\  S  C_  B  /\  ( Gs  S )  e.  Grp ) )
32simp2bi 1011 1  |-  ( S  e.  (SubGrp `  G
)  ->  S  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    e. wcel 1802    C_ wss 3458   ` cfv 5574  (class class class)co 6277   Basecbs 14504   ↾s cress 14505   Grpcgrp 15922  SubGrpcsubg 16064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fv 5582  df-ov 6280  df-subg 16067
This theorem is referenced by:  subgbas  16074  subg0  16076  subginv  16077  subgsubcl  16081  subgsub  16082  subgmulgcl  16083  subgmulg  16084  issubg2  16085  issubg4  16089  subsubg  16093  subgint  16094  nsgconj  16103  nsgacs  16106  ssnmz  16112  eqger  16120  eqgid  16122  eqgen  16123  eqgcpbl  16124  lagsubg2  16131  lagsubg  16132  resghm  16152  ghmnsgima  16159  conjsubg  16167  conjsubgen  16168  conjnmz  16169  conjnmzb  16170  gicsubgen  16195  subgga  16207  gasubg  16209  gastacos  16217  orbstafun  16218  cntrsubgnsg  16247  oddvds2  16457  subgpgp  16486  odcau  16493  pgpssslw  16503  sylow2blem1  16509  sylow2blem2  16510  sylow2blem3  16511  slwhash  16513  fislw  16514  sylow2  16515  sylow3lem1  16516  sylow3lem2  16517  sylow3lem3  16518  sylow3lem4  16519  sylow3lem5  16520  sylow3lem6  16521  lsmval  16537  lsmelval  16538  lsmelvali  16539  lsmelvalm  16540  lsmsubg  16543  lsmub1  16545  lsmub2  16546  lsmless1  16548  lsmless2  16549  lsmless12  16550  lsmass  16557  subglsm  16560  lsmmod  16562  cntzrecd  16565  lsmcntz  16566  lsmcntzr  16567  lsmdisj2  16569  subgdisj1  16578  pj1f  16584  pj1id  16586  pj1lid  16588  pj1rid  16589  pj1ghm  16590  subgabl  16713  ablcntzd  16732  lsmcom  16733  dprdff  16914  dprdffOLD  16920  dprdfadd  16928  dprdfaddOLD  16935  dprdres  16943  dprdss  16944  subgdmdprd  16949  dprdcntz2  16954  dmdprdsplit2lem  16962  ablfacrp  16985  ablfac1eu  16992  pgpfac1lem1  16993  pgpfac1lem2  16994  pgpfac1lem3a  16995  pgpfac1lem3  16996  pgpfac1lem4  16997  pgpfac1lem5  16998  pgpfaclem1  17000  pgpfaclem2  17001  pgpfaclem3  17002  ablfaclem3  17006  ablfac2  17008  issubrg2  17317  issubrg3  17325  islss4  17476  mpllsslem  17962  mpllsslemOLD  17964  subgtgp  20470  subgntr  20471  opnsubg  20472  clssubg  20473  clsnsg  20474  cldsubg  20475  qustgpopn  20484  qustgphaus  20487  tgptsmscls  20518  subgnm  21013  subgngp  21015  lssnlm  21075  efgh  22793  efabl  22802  efsubm  22803  idomsubgmo  31124
  Copyright terms: Public domain W3C validator