Theorem subgss 17979

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

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107   ⊆ wss 3792  ‘cfv 6135  (class class class)co 6922  Basecbs 16255   ↾_s cress 16256  Grpcgrp 17809  SubGrpcsubg 17972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fv 6143  df-ov 6925  df-subg 17975

This theorem is referenced by:  subgbas  17982  subg0  17984  subginv  17985  subgsubcl  17989  subgsub  17990  subgmulgcl  17991  subgmulg  17992  issubg2  17993  issubg4  17997  subsubg  18001  subgint  18002  nsgconj  18011  nsgacs  18014  ssnmz  18020  eqger  18028  eqgid  18030  eqgen  18031  eqgcpbl  18032  lagsubg2  18039  lagsubg  18040  resghm  18060  ghmnsgima  18068  conjsubg  18076  conjsubgen  18077  conjnmz  18078  conjnmzb  18079  gicsubgen  18104  subgga  18116  gasubg  18118  gastacos  18126  orbstafun  18127  cntrsubgnsg  18156  oddvds2  18367  subgpgp  18396  odcau  18403  pgpssslw  18413  sylow2blem1  18419  sylow2blem2  18420  sylow2blem3  18421  slwhash  18423  fislw  18424  sylow2  18425  sylow3lem1  18426  sylow3lem2  18427  sylow3lem3  18428  sylow3lem4  18429  sylow3lem5  18430  sylow3lem6  18431  lsmval  18447  lsmelval  18448  lsmelvali  18449  lsmelvalm  18450  lsmsubg  18453  lsmub1  18455  lsmub2  18456  lsmless1  18458  lsmless2  18459  lsmless12  18460  lsmass  18467  subglsm  18470  lsmmod  18472  cntzrecd  18475  lsmcntz  18476  lsmcntzr  18477  lsmdisj2  18479  subgdisj1  18488  pj1f  18494  pj1id  18496  pj1lid  18498  pj1rid  18499  pj1ghm  18500  subgabl  18627  ablcntzd  18646  lsmcom  18647  dprdff  18798  dprdfadd  18806  dprdres  18814  dprdss  18815  subgdmdprd  18820  dprdcntz2  18824  dmdprdsplit2lem  18831  ablfacrp  18852  ablfac1eu  18859  pgpfac1lem1  18860  pgpfac1lem2  18861  pgpfac1lem3a  18862  pgpfac1lem3  18863  pgpfac1lem4  18864  pgpfac1lem5  18865  pgpfaclem1  18867  pgpfaclem2  18868  pgpfaclem3  18869  ablfaclem3  18873  ablfac2  18875  issubrg2  19192  issubrg3  19200  islss4  19357  mpllsslem  19832  phssip  20401  subgtgp  22317  subgntr  22318  opnsubg  22319  clssubg  22320  clsnsg  22321  cldsubg  22322  qustgpopn  22331  qustgphaus  22334  tgptsmscls  22361  subgnm  22845  subgngp  22847  lssnlm  22913  cmscsscms  23579  efgh  24725  efabl  24734  efsubm  24735  qusker  30407  eqgvscpbl  30408  nelsubgcld  38134  nelsubgsubcld  38135  idomsubgmo  38739