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 1146	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ⊆ wss 3976  ‘cfv 6573  (class class class)co 7448  Basecbs 17258   ↾_s cress 17287  Grpcgrp 18973  SubGrpcsubg 19160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  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  20620  issubrg3  20628  islss4  20983  dflidl2rng  21251  phssip  21699  mpllsslem  22043  subgtgp  24134  subgntr  24136  opnsubg  24137  clssubg  24138  clsnsg  24139  cldsubg  24140  qustgpopn  24149  qustgphaus  24152  tgptsmscls  24179  subgnm  24667  subgngp  24669  lssnlm  24743  cmscsscms  25426  efgh  26601  efabl  26610  efsubm  26611  gsumsubg  33029  qusker  33342  eqgvscpbl  33343  grplsmid  33397  quslsm  33398  qusima  33401  nsgmgc  33405  nsgqusf1olem1  33406  nsgqusf1olem2  33407  nsgqusf1olem3  33408  qsnzr  33448  opprqusplusg  33482  opprqus0g  33483  algextdeglem1  33708  algextdeglem2  33709  algextdeglem3  33710  algextdeglem4  33711  algextdeglem5  33712  nelsubgcld  42452  nelsubgsubcld  42453  idomsubgmo  43154