Theorem subgss 19103

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3889  ‘cfv 6498  (class class class)co 7367  Basecbs 17179   ↾_s cress 17200  Grpcgrp 18909  SubGrpcsubg 19096

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fv 6506  df-ov 7370  df-subg 19099

This theorem is referenced by:  subgbas  19106  subg0  19108  subginv  19109  subgsubcl  19113  subgsub  19114  subgmulgcl  19115  subgmulg  19116  issubg2  19117  issubg4  19121  subsubg  19125  subgint  19126  trivsubgd  19128  nsgconj  19134  nsgacs  19137  ssnmz  19141  eqger  19153  eqgid  19155  eqgen  19156  eqgcpbl  19157  lagsubg2  19169  lagsubg  19170  eqg0subg  19171  resghm  19207  ghmnsgima  19215  conjsubg  19225  conjsubgen  19226  conjnmz  19227  conjnmzb  19228  gicsubgen  19254  ghmqusnsglem1  19255  ghmquskerlem1  19258  subgga  19275  gasubg  19277  gastacos  19285  orbstafun  19286  cntrsubgnsg  19318  oddvds2  19541  subgpgp  19572  odcau  19579  pgpssslw  19589  sylow2blem1  19595  sylow2blem2  19596  sylow2blem3  19597  slwhash  19599  fislw  19600  sylow2  19601  sylow3lem1  19602  sylow3lem2  19603  sylow3lem3  19604  sylow3lem4  19605  sylow3lem5  19606  sylow3lem6  19607  lsmval  19623  lsmelval  19624  lsmelvali  19625  lsmelvalm  19626  lsmsubg  19629  lsmub1  19632  lsmub2  19633  lsmless1  19635  lsmless2  19636  lsmless12  19637  lsmass  19644  subglsm  19648  lsmmod  19650  cntzrecd  19653  lsmcntz  19654  lsmcntzr  19655  lsmdisj2  19657  subgdisj1  19666  pj1f  19672  pj1id  19674  pj1lid  19676  pj1rid  19677  pj1ghm  19678  qusecsub  19810  subgabl  19811  ablcntzd  19832  lsmcom  19833  dprdff  19989  dprdfadd  19997  dprdres  20005  dprdss  20006  subgdmdprd  20011  dprdcntz2  20015  dmdprdsplit2lem  20022  ablfacrp  20043  ablfac1eu  20050  pgpfac1lem1  20051  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem4  20055  pgpfac1lem5  20056  pgpfaclem1  20058  pgpfaclem2  20059  pgpfaclem3  20060  ablfaclem3  20064  ablfac2  20066  prmgrpsimpgd  20091  issubrng2  20535  issubrg2  20569  issubrg3  20577  islss4  20957  dflidl2rng  21216  phssip  21638  mpllsslem  21978  subgtgp  24070  subgntr  24072  opnsubg  24073  clssubg  24074  clsnsg  24075  cldsubg  24076  qustgpopn  24085  qustgphaus  24088  tgptsmscls  24115  subgnm  24598  subgngp  24600  lssnlm  24666  cmscsscms  25340  efgh  26505  efabl  26514  efsubm  26515  subgmulgcld  33104  gsumsubg  33107  qusker  33409  eqgvscpbl  33410  grplsmid  33464  quslsm  33465  qusima  33468  nsgmgc  33472  nsgqusf1olem1  33473  nsgqusf1olem2  33474  nsgqusf1olem3  33475  qsnzr  33515  opprqusplusg  33549  opprqus0g  33550  algextdeglem1  33861  algextdeglem2  33862  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  nelsubgcld  42942  nelsubgsubcld  42943  idomsubgmo  43621