Theorem subgss 18756

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ⊆ wss 3887  ‘cfv 6433  (class class class)co 7275  Basecbs 16912   ↾_s cress 16941  Grpcgrp 18577  SubGrpcsubg 18749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-subg 18752

This theorem is referenced by:  subgbas  18759  subg0  18761  subginv  18762  subgsubcl  18766  subgsub  18767  subgmulgcl  18768  subgmulg  18769  issubg2  18770  issubg4  18774  subsubg  18778  subgint  18779  trivsubgd  18781  nsgconj  18787  nsgacs  18790  ssnmz  18794  eqger  18806  eqgid  18808  eqgen  18809  eqgcpbl  18810  lagsubg2  18817  lagsubg  18818  resghm  18850  ghmnsgima  18858  conjsubg  18866  conjsubgen  18867  conjnmz  18868  conjnmzb  18869  gicsubgen  18894  subgga  18906  gasubg  18908  gastacos  18916  orbstafun  18917  cntrsubgnsg  18947  oddvds2  19173  subgpgp  19202  odcau  19209  pgpssslw  19219  sylow2blem1  19225  sylow2blem2  19226  sylow2blem3  19227  slwhash  19229  fislw  19230  sylow2  19231  sylow3lem1  19232  sylow3lem2  19233  sylow3lem3  19234  sylow3lem4  19235  sylow3lem5  19236  sylow3lem6  19237  lsmval  19253  lsmelval  19254  lsmelvali  19255  lsmelvalm  19256  lsmsubg  19259  lsmub1  19262  lsmub2  19263  lsmless1  19265  lsmless2  19266  lsmless12  19267  lsmass  19275  subglsm  19279  lsmmod  19281  cntzrecd  19284  lsmcntz  19285  lsmcntzr  19286  lsmdisj2  19288  subgdisj1  19297  pj1f  19303  pj1id  19305  pj1lid  19307  pj1rid  19308  pj1ghm  19309  subgabl  19437  ablcntzd  19458  lsmcom  19459  dprdff  19615  dprdfadd  19623  dprdres  19631  dprdss  19632  subgdmdprd  19637  dprdcntz2  19641  dmdprdsplit2lem  19648  ablfacrp  19669  ablfac1eu  19676  pgpfac1lem1  19677  pgpfac1lem2  19678  pgpfac1lem3a  19679  pgpfac1lem3  19680  pgpfac1lem4  19681  pgpfac1lem5  19682  pgpfaclem1  19684  pgpfaclem2  19685  pgpfaclem3  19686  ablfaclem3  19690  ablfac2  19692  prmgrpsimpgd  19717  issubrg2  20044  issubrg3  20052  islss4  20224  phssip  20863  mpllsslem  21206  subgtgp  23256  subgntr  23258  opnsubg  23259  clssubg  23260  clsnsg  23261  cldsubg  23262  qustgpopn  23271  qustgphaus  23274  tgptsmscls  23301  subgnm  23789  subgngp  23791  lssnlm  23865  cmscsscms  24537  efgh  25697  efabl  25706  efsubm  25707  gsumsubg  31306  qusker  31549  eqgvscpbl  31550  grplsmid  31592  quslsm  31593  qusima  31594  nsgmgc  31597  nsgqusf1olem1  31598  nsgqusf1olem2  31599  nsgqusf1olem3  31600  nelsubgcld  40221  nelsubgsubcld  40222  idomsubgmo  41023