Theorem subgss 19006

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ⊆ wss 3948  ‘cfv 6543  (class class class)co 7408  Basecbs 17143   ↾_s cress 17172  Grpcgrp 18818  SubGrpcsubg 18999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7411  df-subg 19002

This theorem is referenced by:  subgbas  19009  subg0  19011  subginv  19012  subgsubcl  19016  subgsub  19017  subgmulgcl  19018  subgmulg  19019  issubg2  19020  issubg4  19024  subsubg  19028  subgint  19029  trivsubgd  19032  nsgconj  19038  nsgacs  19041  ssnmz  19045  eqger  19057  eqgid  19059  eqgen  19060  eqgcpbl  19061  lagsubg2  19070  lagsubg  19071  eqg0subg  19072  resghm  19107  ghmnsgima  19115  conjsubg  19123  conjsubgen  19124  conjnmz  19125  conjnmzb  19126  gicsubgen  19151  subgga  19163  gasubg  19165  gastacos  19173  orbstafun  19174  cntrsubgnsg  19206  oddvds2  19433  subgpgp  19464  odcau  19471  pgpssslw  19481  sylow2blem1  19487  sylow2blem2  19488  sylow2blem3  19489  slwhash  19491  fislw  19492  sylow2  19493  sylow3lem1  19494  sylow3lem2  19495  sylow3lem3  19496  sylow3lem4  19497  sylow3lem5  19498  sylow3lem6  19499  lsmval  19515  lsmelval  19516  lsmelvali  19517  lsmelvalm  19518  lsmsubg  19521  lsmub1  19524  lsmub2  19525  lsmless1  19527  lsmless2  19528  lsmless12  19529  lsmass  19536  subglsm  19540  lsmmod  19542  cntzrecd  19545  lsmcntz  19546  lsmcntzr  19547  lsmdisj2  19549  subgdisj1  19558  pj1f  19564  pj1id  19566  pj1lid  19568  pj1rid  19569  pj1ghm  19570  qusecsub  19702  subgabl  19703  ablcntzd  19724  lsmcom  19725  dprdff  19881  dprdfadd  19889  dprdres  19897  dprdss  19898  subgdmdprd  19903  dprdcntz2  19907  dmdprdsplit2lem  19914  ablfacrp  19935  ablfac1eu  19942  pgpfac1lem1  19943  pgpfac1lem2  19944  pgpfac1lem3a  19945  pgpfac1lem3  19946  pgpfac1lem4  19947  pgpfac1lem5  19948  pgpfaclem1  19950  pgpfaclem2  19951  pgpfaclem3  19952  ablfaclem3  19956  ablfac2  19958  prmgrpsimpgd  19983  issubrg2  20338  issubrg3  20346  islss4  20572  dflidl2lem  20841  phssip  21210  mpllsslem  21558  subgtgp  23608  subgntr  23610  opnsubg  23611  clssubg  23612  clsnsg  23613  cldsubg  23614  qustgpopn  23623  qustgphaus  23626  tgptsmscls  23653  subgnm  24141  subgngp  24143  lssnlm  24217  cmscsscms  24889  efgh  26049  efabl  26058  efsubm  26059  gsumsubg  32193  qusker  32459  eqgvscpbl  32460  grplsmid  32509  quslsm  32511  qusima  32514  nsgmgc  32518  nsgqusf1olem1  32519  nsgqusf1olem2  32520  nsgqusf1olem3  32521  ghmquskerlem1  32523  qsnzr  32569  opprqusplusg  32598  opprqus0g  32599  algextdeglem1  32767  nelsubgcld  41073  nelsubgsubcld  41074  idomsubgmo  41930  issubrng2  46727  dflidl2rng  46740