Theorem subgss 19050

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105   ⊆ wss 3948  ‘cfv 6543  (class class class)co 7412  Basecbs 17151   ↾_s cress 17180  Grpcgrp 18861  SubGrpcsubg 19043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  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 7415  df-subg 19046

This theorem is referenced by:  subgbas  19053  subg0  19055  subginv  19056  subgsubcl  19060  subgsub  19061  subgmulgcl  19062  subgmulg  19063  issubg2  19064  issubg4  19068  subsubg  19072  subgint  19073  trivsubgd  19076  nsgconj  19082  nsgacs  19085  ssnmz  19089  eqger  19101  eqgid  19103  eqgen  19104  eqgcpbl  19105  lagsubg2  19116  lagsubg  19117  eqg0subg  19118  resghm  19153  ghmnsgima  19161  conjsubg  19171  conjsubgen  19172  conjnmz  19173  conjnmzb  19174  gicsubgen  19200  subgga  19212  gasubg  19214  gastacos  19222  orbstafun  19223  cntrsubgnsg  19255  oddvds2  19482  subgpgp  19513  odcau  19520  pgpssslw  19530  sylow2blem1  19536  sylow2blem2  19537  sylow2blem3  19538  slwhash  19540  fislw  19541  sylow2  19542  sylow3lem1  19543  sylow3lem2  19544  sylow3lem3  19545  sylow3lem4  19546  sylow3lem5  19547  sylow3lem6  19548  lsmval  19564  lsmelval  19565  lsmelvali  19566  lsmelvalm  19567  lsmsubg  19570  lsmub1  19573  lsmub2  19574  lsmless1  19576  lsmless2  19577  lsmless12  19578  lsmass  19585  subglsm  19589  lsmmod  19591  cntzrecd  19594  lsmcntz  19595  lsmcntzr  19596  lsmdisj2  19598  subgdisj1  19607  pj1f  19613  pj1id  19615  pj1lid  19617  pj1rid  19618  pj1ghm  19619  qusecsub  19751  subgabl  19752  ablcntzd  19773  lsmcom  19774  dprdff  19930  dprdfadd  19938  dprdres  19946  dprdss  19947  subgdmdprd  19952  dprdcntz2  19956  dmdprdsplit2lem  19963  ablfacrp  19984  ablfac1eu  19991  pgpfac1lem1  19992  pgpfac1lem2  19993  pgpfac1lem3a  19994  pgpfac1lem3  19995  pgpfac1lem4  19996  pgpfac1lem5  19997  pgpfaclem1  19999  pgpfaclem2  20000  pgpfaclem3  20001  ablfaclem3  20005  ablfac2  20007  prmgrpsimpgd  20032  issubrng2  20454  issubrg2  20490  issubrg3  20498  islss4  20805  dflidl2lem  21080  dflidl2rng  21119  phssip  21521  mpllsslem  21870  subgtgp  23929  subgntr  23931  opnsubg  23932  clssubg  23933  clsnsg  23934  cldsubg  23935  qustgpopn  23944  qustgphaus  23947  tgptsmscls  23974  subgnm  24462  subgngp  24464  lssnlm  24538  cmscsscms  25221  efgh  26390  efabl  26399  efsubm  26400  gsumsubg  32634  qusker  32900  eqgvscpbl  32901  grplsmid  32954  quslsm  32956  qusima  32959  nsgmgc  32963  nsgqusf1olem1  32964  nsgqusf1olem2  32965  nsgqusf1olem3  32966  ghmquskerlem1  32968  qsnzr  33014  opprqusplusg  33043  opprqus0g  33044  algextdeglem1  33228  algextdeglem2  33229  algextdeglem3  33230  algextdeglem4  33231  algextdeglem5  33232  nelsubgcld  41538  nelsubgsubcld  41539  idomsubgmo  42403