Theorem subgss 18737

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109   ⊆ wss 3891  ‘cfv 6430  (class class class)co 7268  Basecbs 16893   ↾_s cress 16922  Grpcgrp 18558  SubGrpcsubg 18730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fv 6438  df-ov 7271  df-subg 18733

This theorem is referenced by:  subgbas  18740  subg0  18742  subginv  18743  subgsubcl  18747  subgsub  18748  subgmulgcl  18749  subgmulg  18750  issubg2  18751  issubg4  18755  subsubg  18759  subgint  18760  trivsubgd  18762  nsgconj  18768  nsgacs  18771  ssnmz  18775  eqger  18787  eqgid  18789  eqgen  18790  eqgcpbl  18791  lagsubg2  18798  lagsubg  18799  resghm  18831  ghmnsgima  18839  conjsubg  18847  conjsubgen  18848  conjnmz  18849  conjnmzb  18850  gicsubgen  18875  subgga  18887  gasubg  18889  gastacos  18897  orbstafun  18898  cntrsubgnsg  18928  oddvds2  19154  subgpgp  19183  odcau  19190  pgpssslw  19200  sylow2blem1  19206  sylow2blem2  19207  sylow2blem3  19208  slwhash  19210  fislw  19211  sylow2  19212  sylow3lem1  19213  sylow3lem2  19214  sylow3lem3  19215  sylow3lem4  19216  sylow3lem5  19217  sylow3lem6  19218  lsmval  19234  lsmelval  19235  lsmelvali  19236  lsmelvalm  19237  lsmsubg  19240  lsmub1  19243  lsmub2  19244  lsmless1  19246  lsmless2  19247  lsmless12  19248  lsmass  19256  subglsm  19260  lsmmod  19262  cntzrecd  19265  lsmcntz  19266  lsmcntzr  19267  lsmdisj2  19269  subgdisj1  19278  pj1f  19284  pj1id  19286  pj1lid  19288  pj1rid  19289  pj1ghm  19290  subgabl  19418  ablcntzd  19439  lsmcom  19440  dprdff  19596  dprdfadd  19604  dprdres  19612  dprdss  19613  subgdmdprd  19618  dprdcntz2  19622  dmdprdsplit2lem  19629  ablfacrp  19650  ablfac1eu  19657  pgpfac1lem1  19658  pgpfac1lem2  19659  pgpfac1lem3a  19660  pgpfac1lem3  19661  pgpfac1lem4  19662  pgpfac1lem5  19663  pgpfaclem1  19665  pgpfaclem2  19666  pgpfaclem3  19667  ablfaclem3  19671  ablfac2  19673  prmgrpsimpgd  19698  issubrg2  20025  issubrg3  20033  islss4  20205  phssip  20844  mpllsslem  21187  subgtgp  23237  subgntr  23239  opnsubg  23240  clssubg  23241  clsnsg  23242  cldsubg  23243  qustgpopn  23252  qustgphaus  23255  tgptsmscls  23282  subgnm  23770  subgngp  23772  lssnlm  23846  cmscsscms  24518  efgh  25678  efabl  25687  efsubm  25688  gsumsubg  31285  qusker  31528  eqgvscpbl  31529  grplsmid  31571  quslsm  31572  qusima  31573  nsgmgc  31576  nsgqusf1olem1  31577  nsgqusf1olem2  31578  nsgqusf1olem3  31579  nelsubgcld  40201  nelsubgsubcld  40202  idomsubgmo  41003