Theorem subgss 18282

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   ⊆ wss 3938  ‘cfv 6357  (class class class)co 7158  Basecbs 16485   ↾_s cress 16486  Grpcgrp 18105  SubGrpcsubg 18275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fv 6365  df-ov 7161  df-subg 18278

This theorem is referenced by:  subgbas  18285  subg0  18287  subginv  18288  subgsubcl  18292  subgsub  18293  subgmulgcl  18294  subgmulg  18295  issubg2  18296  issubg4  18300  subsubg  18304  subgint  18305  trivsubgd  18307  nsgconj  18313  nsgacs  18316  ssnmz  18320  eqger  18332  eqgid  18334  eqgen  18335  eqgcpbl  18336  lagsubg2  18343  lagsubg  18344  resghm  18376  ghmnsgima  18384  conjsubg  18392  conjsubgen  18393  conjnmz  18394  conjnmzb  18395  gicsubgen  18420  subgga  18432  gasubg  18434  gastacos  18442  orbstafun  18443  cntrsubgnsg  18473  oddvds2  18695  subgpgp  18724  odcau  18731  pgpssslw  18741  sylow2blem1  18747  sylow2blem2  18748  sylow2blem3  18749  slwhash  18751  fislw  18752  sylow2  18753  sylow3lem1  18754  sylow3lem2  18755  sylow3lem3  18756  sylow3lem4  18757  sylow3lem5  18758  sylow3lem6  18759  lsmval  18775  lsmelval  18776  lsmelvali  18777  lsmelvalm  18778  lsmsubg  18781  lsmub1  18784  lsmub2  18785  lsmless1  18787  lsmless2  18788  lsmless12  18789  lsmass  18797  subglsm  18801  lsmmod  18803  cntzrecd  18806  lsmcntz  18807  lsmcntzr  18808  lsmdisj2  18810  subgdisj1  18819  pj1f  18825  pj1id  18827  pj1lid  18829  pj1rid  18830  pj1ghm  18831  subgabl  18958  ablcntzd  18979  lsmcom  18980  dprdff  19136  dprdfadd  19144  dprdres  19152  dprdss  19153  subgdmdprd  19158  dprdcntz2  19162  dmdprdsplit2lem  19169  ablfacrp  19190  ablfac1eu  19197  pgpfac1lem1  19198  pgpfac1lem2  19199  pgpfac1lem3a  19200  pgpfac1lem3  19201  pgpfac1lem4  19202  pgpfac1lem5  19203  pgpfaclem1  19205  pgpfaclem2  19206  pgpfaclem3  19207  ablfaclem3  19211  ablfac2  19213  prmgrpsimpgd  19238  issubrg2  19557  issubrg3  19565  islss4  19736  mpllsslem  20217  phssip  20804  subgtgp  22715  subgntr  22717  opnsubg  22718  clssubg  22719  clsnsg  22720  cldsubg  22721  qustgpopn  22730  qustgphaus  22733  tgptsmscls  22760  subgnm  23244  subgngp  23246  lssnlm  23312  cmscsscms  23978  efgh  25127  efabl  25136  efsubm  25137  gsumsubg  30686  qusker  30920  eqgvscpbl  30921  nelsubgcld  39136  nelsubgsubcld  39137  idomsubgmo  39805