Theorem subgss 19113

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ⊆ wss 3931  ‘cfv 6540  (class class class)co 7412  Basecbs 17228   ↾_s cress 17251  Grpcgrp 18919  SubGrpcsubg 19106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6493  df-fun 6542  df-fv 6548  df-ov 7415  df-subg 19109

This theorem is referenced by:  subgbas  19116  subg0  19118  subginv  19119  subgsubcl  19123  subgsub  19124  subgmulgcl  19125  subgmulg  19126  issubg2  19127  issubg4  19131  subsubg  19135  subgint  19136  trivsubgd  19139  nsgconj  19145  nsgacs  19148  ssnmz  19152  eqger  19164  eqgid  19166  eqgen  19167  eqgcpbl  19168  lagsubg2  19180  lagsubg  19181  eqg0subg  19182  resghm  19218  ghmnsgima  19226  conjsubg  19236  conjsubgen  19237  conjnmz  19238  conjnmzb  19239  gicsubgen  19265  ghmqusnsglem1  19266  ghmquskerlem1  19269  subgga  19286  gasubg  19288  gastacos  19296  orbstafun  19297  cntrsubgnsg  19329  oddvds2  19551  subgpgp  19582  odcau  19589  pgpssslw  19599  sylow2blem1  19605  sylow2blem2  19606  sylow2blem3  19607  slwhash  19609  fislw  19610  sylow2  19611  sylow3lem1  19612  sylow3lem2  19613  sylow3lem3  19614  sylow3lem4  19615  sylow3lem5  19616  sylow3lem6  19617  lsmval  19633  lsmelval  19634  lsmelvali  19635  lsmelvalm  19636  lsmsubg  19639  lsmub1  19642  lsmub2  19643  lsmless1  19645  lsmless2  19646  lsmless12  19647  lsmass  19654  subglsm  19658  lsmmod  19660  cntzrecd  19663  lsmcntz  19664  lsmcntzr  19665  lsmdisj2  19667  subgdisj1  19676  pj1f  19682  pj1id  19684  pj1lid  19686  pj1rid  19687  pj1ghm  19688  qusecsub  19820  subgabl  19821  ablcntzd  19842  lsmcom  19843  dprdff  19999  dprdfadd  20007  dprdres  20015  dprdss  20016  subgdmdprd  20021  dprdcntz2  20025  dmdprdsplit2lem  20032  ablfacrp  20053  ablfac1eu  20060  pgpfac1lem1  20061  pgpfac1lem2  20062  pgpfac1lem3a  20063  pgpfac1lem3  20064  pgpfac1lem4  20065  pgpfac1lem5  20066  pgpfaclem1  20068  pgpfaclem2  20069  pgpfaclem3  20070  ablfaclem3  20074  ablfac2  20076  prmgrpsimpgd  20101  issubrng2  20525  issubrg2  20559  issubrg3  20567  islss4  20927  dflidl2rng  21189  phssip  21629  mpllsslem  21973  subgtgp  24058  subgntr  24060  opnsubg  24061  clssubg  24062  clsnsg  24063  cldsubg  24064  qustgpopn  24073  qustgphaus  24076  tgptsmscls  24103  subgnm  24589  subgngp  24591  lssnlm  24657  cmscsscms  25342  efgh  26518  efabl  26527  efsubm  26528  subgmulgcld  32978  gsumsubg  32979  qusker  33303  eqgvscpbl  33304  grplsmid  33358  quslsm  33359  qusima  33362  nsgmgc  33366  nsgqusf1olem1  33367  nsgqusf1olem2  33368  nsgqusf1olem3  33369  qsnzr  33409  opprqusplusg  33443  opprqus0g  33444  algextdeglem1  33688  algextdeglem2  33689  algextdeglem3  33690  algextdeglem4  33691  algextdeglem5  33692  nelsubgcld  42445  nelsubgsubcld  42446  idomsubgmo  43143