Theorem subgss 19059

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901  ‘cfv 6492  (class class class)co 7358  Basecbs 17138   ↾_s cress 17159  Grpcgrp 18865  SubGrpcsubg 19052

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-subg 19055

This theorem is referenced by:  subgbas  19062  subg0  19064  subginv  19065  subgsubcl  19069  subgsub  19070  subgmulgcl  19071  subgmulg  19072  issubg2  19073  issubg4  19077  subsubg  19081  subgint  19082  trivsubgd  19084  nsgconj  19090  nsgacs  19093  ssnmz  19097  eqger  19109  eqgid  19111  eqgen  19112  eqgcpbl  19113  lagsubg2  19125  lagsubg  19126  eqg0subg  19127  resghm  19163  ghmnsgima  19171  conjsubg  19181  conjsubgen  19182  conjnmz  19183  conjnmzb  19184  gicsubgen  19210  ghmqusnsglem1  19211  ghmquskerlem1  19214  subgga  19231  gasubg  19233  gastacos  19241  orbstafun  19242  cntrsubgnsg  19274  oddvds2  19497  subgpgp  19528  odcau  19535  pgpssslw  19545  sylow2blem1  19551  sylow2blem2  19552  sylow2blem3  19553  slwhash  19555  fislw  19556  sylow2  19557  sylow3lem1  19558  sylow3lem2  19559  sylow3lem3  19560  sylow3lem4  19561  sylow3lem5  19562  sylow3lem6  19563  lsmval  19579  lsmelval  19580  lsmelvali  19581  lsmelvalm  19582  lsmsubg  19585  lsmub1  19588  lsmub2  19589  lsmless1  19591  lsmless2  19592  lsmless12  19593  lsmass  19600  subglsm  19604  lsmmod  19606  cntzrecd  19609  lsmcntz  19610  lsmcntzr  19611  lsmdisj2  19613  subgdisj1  19622  pj1f  19628  pj1id  19630  pj1lid  19632  pj1rid  19633  pj1ghm  19634  qusecsub  19766  subgabl  19767  ablcntzd  19788  lsmcom  19789  dprdff  19945  dprdfadd  19953  dprdres  19961  dprdss  19962  subgdmdprd  19967  dprdcntz2  19971  dmdprdsplit2lem  19978  ablfacrp  19999  ablfac1eu  20006  pgpfac1lem1  20007  pgpfac1lem2  20008  pgpfac1lem3a  20009  pgpfac1lem3  20010  pgpfac1lem4  20011  pgpfac1lem5  20012  pgpfaclem1  20014  pgpfaclem2  20015  pgpfaclem3  20016  ablfaclem3  20020  ablfac2  20022  prmgrpsimpgd  20047  issubrng2  20493  issubrg2  20527  issubrg3  20535  islss4  20915  dflidl2rng  21175  phssip  21615  mpllsslem  21957  subgtgp  24051  subgntr  24053  opnsubg  24054  clssubg  24055  clsnsg  24056  cldsubg  24057  qustgpopn  24066  qustgphaus  24069  tgptsmscls  24096  subgnm  24579  subgngp  24581  lssnlm  24647  cmscsscms  25331  efgh  26508  efabl  26517  efsubm  26518  subgmulgcld  33128  gsumsubg  33131  qusker  33432  eqgvscpbl  33433  grplsmid  33487  quslsm  33488  qusima  33491  nsgmgc  33495  nsgqusf1olem1  33496  nsgqusf1olem2  33497  nsgqusf1olem3  33498  qsnzr  33538  opprqusplusg  33572  opprqus0g  33573  algextdeglem1  33876  algextdeglem2  33877  algextdeglem3  33878  algextdeglem4  33879  algextdeglem5  33880  nelsubgcld  42773  nelsubgsubcld  42774  idomsubgmo  43456