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 1540   ∈ wcel 2109   ⊆ wss 3903  ‘cfv 6482  (class class class)co 7349  Basecbs 17120   ↾_s cress 17141  Grpcgrp 18812  SubGrpcsubg 18999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fv 6490  df-ov 7352  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  19073  lagsubg  19074  eqg0subg  19075  resghm  19111  ghmnsgima  19119  conjsubg  19129  conjsubgen  19130  conjnmz  19131  conjnmzb  19132  gicsubgen  19158  ghmqusnsglem1  19159  ghmquskerlem1  19162  subgga  19179  gasubg  19181  gastacos  19189  orbstafun  19190  cntrsubgnsg  19222  oddvds2  19445  subgpgp  19476  odcau  19483  pgpssslw  19493  sylow2blem1  19499  sylow2blem2  19500  sylow2blem3  19501  slwhash  19503  fislw  19504  sylow2  19505  sylow3lem1  19506  sylow3lem2  19507  sylow3lem3  19508  sylow3lem4  19509  sylow3lem5  19510  sylow3lem6  19511  lsmval  19527  lsmelval  19528  lsmelvali  19529  lsmelvalm  19530  lsmsubg  19533  lsmub1  19536  lsmub2  19537  lsmless1  19539  lsmless2  19540  lsmless12  19541  lsmass  19548  subglsm  19552  lsmmod  19554  cntzrecd  19557  lsmcntz  19558  lsmcntzr  19559  lsmdisj2  19561  subgdisj1  19570  pj1f  19576  pj1id  19578  pj1lid  19580  pj1rid  19581  pj1ghm  19582  qusecsub  19714  subgabl  19715  ablcntzd  19736  lsmcom  19737  dprdff  19893  dprdfadd  19901  dprdres  19909  dprdss  19910  subgdmdprd  19915  dprdcntz2  19919  dmdprdsplit2lem  19926  ablfacrp  19947  ablfac1eu  19954  pgpfac1lem1  19955  pgpfac1lem2  19956  pgpfac1lem3a  19957  pgpfac1lem3  19958  pgpfac1lem4  19959  pgpfac1lem5  19960  pgpfaclem1  19962  pgpfaclem2  19963  pgpfaclem3  19964  ablfaclem3  19968  ablfac2  19970  prmgrpsimpgd  19995  issubrng2  20443  issubrg2  20477  issubrg3  20485  islss4  20865  dflidl2rng  21125  phssip  21565  mpllsslem  21907  subgtgp  23990  subgntr  23992  opnsubg  23993  clssubg  23994  clsnsg  23995  cldsubg  23996  qustgpopn  24005  qustgphaus  24008  tgptsmscls  24035  subgnm  24519  subgngp  24521  lssnlm  24587  cmscsscms  25271  efgh  26448  efabl  26457  efsubm  26458  subgmulgcld  32998  gsumsubg  33000  qusker  33287  eqgvscpbl  33288  grplsmid  33342  quslsm  33343  qusima  33346  nsgmgc  33350  nsgqusf1olem1  33351  nsgqusf1olem2  33352  nsgqusf1olem3  33353  qsnzr  33393  opprqusplusg  33427  opprqus0g  33428  algextdeglem1  33690  algextdeglem2  33691  algextdeglem3  33692  algextdeglem4  33693  algextdeglem5  33694  nelsubgcld  42480  nelsubgsubcld  42481  idomsubgmo  43176