Theorem subgss 19188

Description: A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.)

Hypothesis

Ref	Expression
issubg.b	⊢ 𝐵 = (Base‘𝐺)

Assertion

Ref	Expression
subgss	⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)

Proof of Theorem subgss

Step	Hyp	Ref	Expression
1		issubg.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
2	1	issubg 19187	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
3	2	simp2bi 1164	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ⊆ wss 3905  ‘cfv 6536  (class class class)co 7410  Basecbs 17264   ↾_s cress 17285  Grpcgrp 18995  SubGrpcsubg 19181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fv 6544  df-ov 7413  df-subg 19184

This theorem is referenced by:  subgbas  19191  subg0  19193  subginv  19194  subgsubcl  19199  subgsub  19200  subgmulgcl  19201  subgmulg  19202  issubg2  19203  issubg4  19207  subsubg  19211  subgint  19212  trivsubgd  19214  nsgconj  19220  nsgacs  19223  ssnmz  19227  eqger  19241  eqgid  19243  eqgen  19244  eqgcpbl  19245  lagsubg2  19260  lagsubg  19261  eqg0subg  19262  resghm  19297  ghmnsgima  19305  conjsubg  19315  conjsubgen  19316  conjnmz  19317  conjnmzb  19318  gicsubgen  19344  ghmqusnsglem1  19345  ghmquskerlem1  19348  subgga  19365  gasubg  19367  gastacos  19375  orbstafun  19376  cntrsubgnsg  19408  oddvds2  19631  subgpgp  19662  odcau  19669  pgpssslw  19679  sylow2blem1  19685  sylow2blem2  19686  sylow2blem3  19687  slwhash  19689  fislw  19690  sylow2  19691  sylow3lem1  19692  sylow3lem2  19693  sylow3lem3  19694  sylow3lem4  19695  sylow3lem5  19696  sylow3lem6  19697  lsmval  19713  lsmelval  19714  lsmelvali  19715  lsmelvalm  19716  lsmsubg  19719  lsmub1  19722  lsmub2  19723  lsmless1  19725  lsmless2  19726  lsmless12  19727  lsmass  19734  subglsm  19738  lsmmod  19740  cntzrecd  19743  lsmcntz  19744  lsmcntzr  19745  lsmdisj2  19747  subgdisj1  19756  pj1f  19762  pj1id  19764  pj1lid  19766  pj1rid  19767  pj1ghm  19768  qusecsub  19900  subgabl  19901  ablcntzd  19922  lsmcom  19923  dprdff  20079  dprdfadd  20087  dprdres  20095  dprdss  20096  subgdmdprd  20101  dprdcntz2  20105  dmdprdsplit2lem  20112  ablfacrp  20133  ablfac1eu  20140  pgpfac1lem1  20141  pgpfac1lem2  20142  pgpfac1lem3a  20143  pgpfac1lem3  20144  pgpfac1lem4  20145  pgpfac1lem5  20146  pgpfaclem1  20148  pgpfaclem2  20149  pgpfaclem3  20150  ablfaclem3  20154  ablfac2  20156  prmgrpsimpgd  20181  issubrng2  20657  issubrg2  20691  issubrg3  20699  islss4  21083  dflidl2rng  21343  df2idl2crng  21421  qsnzr  21483  phssip  21808  mpllsslem  22149  subgtgp  24262  subgntr  24264  opnsubg  24265  clssubg  24266  clsnsg  24267  cldsubg  24268  qustgpopn  24277  qustgphaus  24280  tgptsmscls  24307  subgnm  24790  subgngp  24792  lssnlm  24858  cmscsscms  25532  efgh  26706  efabl  26715  efsubm  26716  subgmulgcld  33363  gsumsubg  33366  qusker  33669  eqgvscpbl  33670  grplsmid  33713  quslsm  33714  qusima  33717  nsgmgc  33721  nsgqusf1olem1  33722  nsgqusf1olem2  33723  nsgqusf1olem3  33724  opprqusplusg  33771  opprqus0g  33772  algextdeglem1  34107  algextdeglem2  34108  algextdeglem3  34109  algextdeglem4  34110  algextdeglem5  34111  nelsubgcld  43291  nelsubgsubcld  43292  idomsubgmo  43940