Theorem subgss 19040

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ⊆ wss 3897  ‘cfv 6481  (class class class)co 7346  Basecbs 17120   ↾_s cress 17141  Grpcgrp 18846  SubGrpcsubg 19033

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-subg 19036

This theorem is referenced by:  subgbas  19043  subg0  19045  subginv  19046  subgsubcl  19050  subgsub  19051  subgmulgcl  19052  subgmulg  19053  issubg2  19054  issubg4  19058  subsubg  19062  subgint  19063  trivsubgd  19065  nsgconj  19071  nsgacs  19074  ssnmz  19078  eqger  19090  eqgid  19092  eqgen  19093  eqgcpbl  19094  lagsubg2  19106  lagsubg  19107  eqg0subg  19108  resghm  19144  ghmnsgima  19152  conjsubg  19162  conjsubgen  19163  conjnmz  19164  conjnmzb  19165  gicsubgen  19191  ghmqusnsglem1  19192  ghmquskerlem1  19195  subgga  19212  gasubg  19214  gastacos  19222  orbstafun  19223  cntrsubgnsg  19255  oddvds2  19478  subgpgp  19509  odcau  19516  pgpssslw  19526  sylow2blem1  19532  sylow2blem2  19533  sylow2blem3  19534  slwhash  19536  fislw  19537  sylow2  19538  sylow3lem1  19539  sylow3lem2  19540  sylow3lem3  19541  sylow3lem4  19542  sylow3lem5  19543  sylow3lem6  19544  lsmval  19560  lsmelval  19561  lsmelvali  19562  lsmelvalm  19563  lsmsubg  19566  lsmub1  19569  lsmub2  19570  lsmless1  19572  lsmless2  19573  lsmless12  19574  lsmass  19581  subglsm  19585  lsmmod  19587  cntzrecd  19590  lsmcntz  19591  lsmcntzr  19592  lsmdisj2  19594  subgdisj1  19603  pj1f  19609  pj1id  19611  pj1lid  19613  pj1rid  19614  pj1ghm  19615  qusecsub  19747  subgabl  19748  ablcntzd  19769  lsmcom  19770  dprdff  19926  dprdfadd  19934  dprdres  19942  dprdss  19943  subgdmdprd  19948  dprdcntz2  19952  dmdprdsplit2lem  19959  ablfacrp  19980  ablfac1eu  19987  pgpfac1lem1  19988  pgpfac1lem2  19989  pgpfac1lem3a  19990  pgpfac1lem3  19991  pgpfac1lem4  19992  pgpfac1lem5  19993  pgpfaclem1  19995  pgpfaclem2  19996  pgpfaclem3  19997  ablfaclem3  20001  ablfac2  20003  prmgrpsimpgd  20028  issubrng2  20473  issubrg2  20507  issubrg3  20515  islss4  20895  dflidl2rng  21155  phssip  21595  mpllsslem  21937  subgtgp  24020  subgntr  24022  opnsubg  24023  clssubg  24024  clsnsg  24025  cldsubg  24026  qustgpopn  24035  qustgphaus  24038  tgptsmscls  24065  subgnm  24548  subgngp  24550  lssnlm  24616  cmscsscms  25300  efgh  26477  efabl  26486  efsubm  26487  subgmulgcld  33024  gsumsubg  33026  qusker  33314  eqgvscpbl  33315  grplsmid  33369  quslsm  33370  qusima  33373  nsgmgc  33377  nsgqusf1olem1  33378  nsgqusf1olem2  33379  nsgqusf1olem3  33380  qsnzr  33420  opprqusplusg  33454  opprqus0g  33455  algextdeglem1  33730  algextdeglem2  33731  algextdeglem3  33732  algextdeglem4  33733  algextdeglem5  33734  nelsubgcld  42600  nelsubgsubcld  42601  idomsubgmo  43296