Theorem subgss 18671

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 18670	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
3	2	simp2bi 1144	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883  ‘cfv 6418  (class class class)co 7255  Basecbs 16840   ↾_s cress 16867  Grpcgrp 18492  SubGrpcsubg 18664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-subg 18667

This theorem is referenced by:  subgbas  18674  subg0  18676  subginv  18677  subgsubcl  18681  subgsub  18682  subgmulgcl  18683  subgmulg  18684  issubg2  18685  issubg4  18689  subsubg  18693  subgint  18694  trivsubgd  18696  nsgconj  18702  nsgacs  18705  ssnmz  18709  eqger  18721  eqgid  18723  eqgen  18724  eqgcpbl  18725  lagsubg2  18732  lagsubg  18733  resghm  18765  ghmnsgima  18773  conjsubg  18781  conjsubgen  18782  conjnmz  18783  conjnmzb  18784  gicsubgen  18809  subgga  18821  gasubg  18823  gastacos  18831  orbstafun  18832  cntrsubgnsg  18862  oddvds2  19088  subgpgp  19117  odcau  19124  pgpssslw  19134  sylow2blem1  19140  sylow2blem2  19141  sylow2blem3  19142  slwhash  19144  fislw  19145  sylow2  19146  sylow3lem1  19147  sylow3lem2  19148  sylow3lem3  19149  sylow3lem4  19150  sylow3lem5  19151  sylow3lem6  19152  lsmval  19168  lsmelval  19169  lsmelvali  19170  lsmelvalm  19171  lsmsubg  19174  lsmub1  19177  lsmub2  19178  lsmless1  19180  lsmless2  19181  lsmless12  19182  lsmass  19190  subglsm  19194  lsmmod  19196  cntzrecd  19199  lsmcntz  19200  lsmcntzr  19201  lsmdisj2  19203  subgdisj1  19212  pj1f  19218  pj1id  19220  pj1lid  19222  pj1rid  19223  pj1ghm  19224  subgabl  19352  ablcntzd  19373  lsmcom  19374  dprdff  19530  dprdfadd  19538  dprdres  19546  dprdss  19547  subgdmdprd  19552  dprdcntz2  19556  dmdprdsplit2lem  19563  ablfacrp  19584  ablfac1eu  19591  pgpfac1lem1  19592  pgpfac1lem2  19593  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfac1lem4  19596  pgpfac1lem5  19597  pgpfaclem1  19599  pgpfaclem2  19600  pgpfaclem3  19601  ablfaclem3  19605  ablfac2  19607  prmgrpsimpgd  19632  issubrg2  19959  issubrg3  19967  islss4  20139  phssip  20775  mpllsslem  21116  subgtgp  23164  subgntr  23166  opnsubg  23167  clssubg  23168  clsnsg  23169  cldsubg  23170  qustgpopn  23179  qustgphaus  23182  tgptsmscls  23209  subgnm  23695  subgngp  23697  lssnlm  23771  cmscsscms  24442  efgh  25602  efabl  25611  efsubm  25612  gsumsubg  31208  qusker  31451  eqgvscpbl  31452  grplsmid  31494  quslsm  31495  qusima  31496  nsgmgc  31499  nsgqusf1olem1  31500  nsgqusf1olem2  31501  nsgqusf1olem3  31502  nelsubgcld  40147  nelsubgsubcld  40148  idomsubgmo  40939