Theorem subgss 19196

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2150   ⊆ wss 3913  ‘cfv 6540  (class class class)co 7414  Basecbs 17272   ↾_s cress 17293  Grpcgrp 19003  SubGrpcsubg 19189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-11 2199  ax-12 2220  ax-ext 2742  ax-sep 5262  ax-nul 5274  ax-pow 5340  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-nfc 2919  df-ne 2966  df-ral 3087  df-rex 3097  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5560  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7417  df-subg 19192

This theorem is referenced by:  subgbas  19199  subg0  19201  subginv  19202  subgsubcl  19207  subgsub  19208  subgmulgcl  19209  subgmulg  19210  issubg2  19211  issubg4  19215  subsubg  19219  subgint  19220  trivsubgd  19222  nsgconj  19228  nsgacs  19231  ssnmz  19235  eqger  19249  eqgid  19251  eqgen  19252  eqgcpbl  19253  lagsubg2  19268  lagsubg  19269  eqg0subg  19270  resghm  19305  ghmnsgima  19313  conjsubg  19323  conjsubgen  19324  conjnmz  19325  conjnmzb  19326  gicsubgen  19352  ghmqusnsglem1  19353  ghmquskerlem1  19356  subgga  19373  gasubg  19375  gastacos  19383  orbstafun  19384  cntrsubgnsg  19416  oddvds2  19639  subgpgp  19670  odcau  19677  pgpssslw  19687  sylow2blem1  19693  sylow2blem2  19694  sylow2blem3  19695  slwhash  19697  fislw  19698  sylow2  19699  sylow3lem1  19700  sylow3lem2  19701  sylow3lem3  19702  sylow3lem4  19703  sylow3lem5  19704  sylow3lem6  19705  lsmval  19721  lsmelval  19722  lsmelvali  19723  lsmelvalm  19724  lsmsubg  19727  lsmub1  19730  lsmub2  19731  lsmless1  19733  lsmless2  19734  lsmless12  19735  lsmass  19742  subglsm  19746  lsmmod  19748  cntzrecd  19751  lsmcntz  19752  lsmcntzr  19753  lsmdisj2  19755  subgdisj1  19764  pj1f  19770  pj1id  19772  pj1lid  19774  pj1rid  19775  pj1ghm  19776  qusecsub  19908  subgabl  19909  ablcntzd  19930  lsmcom  19931  dprdff  20087  dprdfadd  20095  dprdres  20103  dprdss  20104  subgdmdprd  20109  dprdcntz2  20113  dmdprdsplit2lem  20120  ablfacrp  20141  ablfac1eu  20148  pgpfac1lem1  20149  pgpfac1lem2  20150  pgpfac1lem3a  20151  pgpfac1lem3  20152  pgpfac1lem4  20153  pgpfac1lem5  20154  pgpfaclem1  20156  pgpfaclem2  20157  pgpfaclem3  20158  ablfaclem3  20162  ablfac2  20164  prmgrpsimpgd  20189  issubrng2  20646  issubrg2  20680  issubrg3  20688  islss4  21066  dflidl2rng  21326  df2idl2crng  21404  qsnzr  21466  phssip  21791  mpllsslem  22132  subgtgp  24245  subgntr  24247  opnsubg  24248  clssubg  24249  clsnsg  24250  cldsubg  24251  qustgpopn  24260  qustgphaus  24263  tgptsmscls  24290  subgnm  24773  subgngp  24775  lssnlm  24841  cmscsscms  25515  efgh  26686  efabl  26695  efsubm  26696  subgmulgcld  33333  gsumsubg  33336  qusker  33639  eqgvscpbl  33640  grplsmid  33683  quslsm  33684  qusima  33687  nsgmgc  33691  nsgqusf1olem1  33692  nsgqusf1olem2  33693  nsgqusf1olem3  33694  opprqusplusg  33741  opprqus0g  33742  algextdeglem1  34077  algextdeglem2  34078  algextdeglem3  34079  algextdeglem4  34080  algextdeglem5  34081  nelsubgcld  43221  nelsubgsubcld  43222  idomsubgmo  43872