Theorem subgss 19167

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ⊆ wss 3966  ‘cfv 6569  (class class class)co 7438  Basecbs 17254   ↾_s cress 17283  Grpcgrp 18973  SubGrpcsubg 19160

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5305  ax-nul 5315  ax-pow 5374  ax-pr 5441

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3483  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4916  df-br 5152  df-opab 5214  df-mpt 5235  df-id 5587  df-xp 5699  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-res 5705  df-ima 5706  df-iota 6522  df-fun 6571  df-fv 6577  df-ov 7441  df-subg 19163

This theorem is referenced by:  subgbas  19170  subg0  19172  subginv  19173  subgsubcl  19177  subgsub  19178  subgmulgcl  19179  subgmulg  19180  issubg2  19181  issubg4  19185  subsubg  19189  subgint  19190  trivsubgd  19193  nsgconj  19199  nsgacs  19202  ssnmz  19206  eqger  19218  eqgid  19220  eqgen  19221  eqgcpbl  19222  lagsubg2  19234  lagsubg  19235  eqg0subg  19236  resghm  19272  ghmnsgima  19280  conjsubg  19290  conjsubgen  19291  conjnmz  19292  conjnmzb  19293  gicsubgen  19319  ghmqusnsglem1  19320  ghmquskerlem1  19323  subgga  19340  gasubg  19342  gastacos  19350  orbstafun  19351  cntrsubgnsg  19383  oddvds2  19608  subgpgp  19639  odcau  19646  pgpssslw  19656  sylow2blem1  19662  sylow2blem2  19663  sylow2blem3  19664  slwhash  19666  fislw  19667  sylow2  19668  sylow3lem1  19669  sylow3lem2  19670  sylow3lem3  19671  sylow3lem4  19672  sylow3lem5  19673  sylow3lem6  19674  lsmval  19690  lsmelval  19691  lsmelvali  19692  lsmelvalm  19693  lsmsubg  19696  lsmub1  19699  lsmub2  19700  lsmless1  19702  lsmless2  19703  lsmless12  19704  lsmass  19711  subglsm  19715  lsmmod  19717  cntzrecd  19720  lsmcntz  19721  lsmcntzr  19722  lsmdisj2  19724  subgdisj1  19733  pj1f  19739  pj1id  19741  pj1lid  19743  pj1rid  19744  pj1ghm  19745  qusecsub  19877  subgabl  19878  ablcntzd  19899  lsmcom  19900  dprdff  20056  dprdfadd  20064  dprdres  20072  dprdss  20073  subgdmdprd  20078  dprdcntz2  20082  dmdprdsplit2lem  20089  ablfacrp  20110  ablfac1eu  20117  pgpfac1lem1  20118  pgpfac1lem2  20119  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfac1lem4  20122  pgpfac1lem5  20123  pgpfaclem1  20125  pgpfaclem2  20126  pgpfaclem3  20127  ablfaclem3  20131  ablfac2  20133  prmgrpsimpgd  20158  issubrng2  20584  issubrg2  20618  issubrg3  20626  islss4  20987  dflidl2rng  21255  phssip  21703  mpllsslem  22047  subgtgp  24138  subgntr  24140  opnsubg  24141  clssubg  24142  clsnsg  24143  cldsubg  24144  qustgpopn  24153  qustgphaus  24156  tgptsmscls  24183  subgnm  24671  subgngp  24673  lssnlm  24747  cmscsscms  25432  efgh  26609  efabl  26618  efsubm  26619  subgmulgcld  33063  gsumsubg  33064  qusker  33389  eqgvscpbl  33390  grplsmid  33444  quslsm  33445  qusima  33448  nsgmgc  33452  nsgqusf1olem1  33453  nsgqusf1olem2  33454  nsgqusf1olem3  33455  qsnzr  33495  opprqusplusg  33529  opprqus0g  33530  algextdeglem1  33755  algextdeglem2  33756  algextdeglem3  33757  algextdeglem4  33758  algextdeglem5  33759  nelsubgcld  42500  nelsubgsubcld  42501  idomsubgmo  43198