Theorem subgss 19072

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3903  ‘cfv 6500  (class class class)co 7368  Basecbs 17148   ↾_s cress 17169  Grpcgrp 18878  SubGrpcsubg 19065

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 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-subg 19068

This theorem is referenced by:  subgbas  19075  subg0  19077  subginv  19078  subgsubcl  19082  subgsub  19083  subgmulgcl  19084  subgmulg  19085  issubg2  19086  issubg4  19090  subsubg  19094  subgint  19095  trivsubgd  19097  nsgconj  19103  nsgacs  19106  ssnmz  19110  eqger  19122  eqgid  19124  eqgen  19125  eqgcpbl  19126  lagsubg2  19138  lagsubg  19139  eqg0subg  19140  resghm  19176  ghmnsgima  19184  conjsubg  19194  conjsubgen  19195  conjnmz  19196  conjnmzb  19197  gicsubgen  19223  ghmqusnsglem1  19224  ghmquskerlem1  19227  subgga  19244  gasubg  19246  gastacos  19254  orbstafun  19255  cntrsubgnsg  19287  oddvds2  19510  subgpgp  19541  odcau  19548  pgpssslw  19558  sylow2blem1  19564  sylow2blem2  19565  sylow2blem3  19566  slwhash  19568  fislw  19569  sylow2  19570  sylow3lem1  19571  sylow3lem2  19572  sylow3lem3  19573  sylow3lem4  19574  sylow3lem5  19575  sylow3lem6  19576  lsmval  19592  lsmelval  19593  lsmelvali  19594  lsmelvalm  19595  lsmsubg  19598  lsmub1  19601  lsmub2  19602  lsmless1  19604  lsmless2  19605  lsmless12  19606  lsmass  19613  subglsm  19617  lsmmod  19619  cntzrecd  19622  lsmcntz  19623  lsmcntzr  19624  lsmdisj2  19626  subgdisj1  19635  pj1f  19641  pj1id  19643  pj1lid  19645  pj1rid  19646  pj1ghm  19647  qusecsub  19779  subgabl  19780  ablcntzd  19801  lsmcom  19802  dprdff  19958  dprdfadd  19966  dprdres  19974  dprdss  19975  subgdmdprd  19980  dprdcntz2  19984  dmdprdsplit2lem  19991  ablfacrp  20012  ablfac1eu  20019  pgpfac1lem1  20020  pgpfac1lem2  20021  pgpfac1lem3a  20022  pgpfac1lem3  20023  pgpfac1lem4  20024  pgpfac1lem5  20025  pgpfaclem1  20027  pgpfaclem2  20028  pgpfaclem3  20029  ablfaclem3  20033  ablfac2  20035  prmgrpsimpgd  20060  issubrng2  20506  issubrg2  20540  issubrg3  20548  islss4  20928  dflidl2rng  21188  phssip  21628  mpllsslem  21970  subgtgp  24064  subgntr  24066  opnsubg  24067  clssubg  24068  clsnsg  24069  cldsubg  24070  qustgpopn  24079  qustgphaus  24082  tgptsmscls  24109  subgnm  24592  subgngp  24594  lssnlm  24660  cmscsscms  25344  efgh  26521  efabl  26530  efsubm  26531  subgmulgcld  33141  gsumsubg  33144  qusker  33446  eqgvscpbl  33447  grplsmid  33501  quslsm  33502  qusima  33505  nsgmgc  33509  nsgqusf1olem1  33510  nsgqusf1olem2  33511  nsgqusf1olem3  33512  qsnzr  33552  opprqusplusg  33586  opprqus0g  33587  algextdeglem1  33899  algextdeglem2  33900  algextdeglem3  33901  algextdeglem4  33902  algextdeglem5  33903  nelsubgcld  42871  nelsubgsubcld  42872  idomsubgmo  43554