Theorem subgss 19169

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142   ⊆ wss 3904  ‘cfv 6521  (class class class)co 7396  Basecbs 17245   ↾_s cress 17266  Grpcgrp 18975  SubGrpcsubg 19162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fv 6529  df-ov 7399  df-subg 19165

This theorem is referenced by:  subgbas  19172  subg0  19174  subginv  19175  subgsubcl  19179  subgsub  19180  subgmulgcl  19181  subgmulg  19182  issubg2  19183  issubg4  19187  subsubg  19191  subgint  19192  trivsubgd  19194  nsgconj  19200  nsgacs  19203  ssnmz  19207  eqger  19219  eqgid  19221  eqgen  19222  eqgcpbl  19223  lagsubg2  19235  lagsubg  19236  eqg0subg  19237  resghm  19272  ghmnsgima  19280  conjsubg  19290  conjsubgen  19291  conjnmz  19292  conjnmzb  19293  gicsubgen  19319  ghmqusnsglem1  19320  ghmquskerlem1  19323  subgga  19340  gasubg  19342  gastacos  19350  orbstafun  19351  cntrsubgnsg  19383  oddvds2  19606  subgpgp  19637  odcau  19644  pgpssslw  19654  sylow2blem1  19660  sylow2blem2  19661  sylow2blem3  19662  slwhash  19664  fislw  19665  sylow2  19666  sylow3lem1  19667  sylow3lem2  19668  sylow3lem3  19669  sylow3lem4  19670  sylow3lem5  19671  sylow3lem6  19672  lsmval  19688  lsmelval  19689  lsmelvali  19690  lsmelvalm  19691  lsmsubg  19694  lsmub1  19697  lsmub2  19698  lsmless1  19700  lsmless2  19701  lsmless12  19702  lsmass  19709  subglsm  19713  lsmmod  19715  cntzrecd  19718  lsmcntz  19719  lsmcntzr  19720  lsmdisj2  19722  subgdisj1  19731  pj1f  19737  pj1id  19739  pj1lid  19741  pj1rid  19742  pj1ghm  19743  qusecsub  19875  subgabl  19876  ablcntzd  19897  lsmcom  19898  dprdff  20054  dprdfadd  20062  dprdres  20070  dprdss  20071  subgdmdprd  20076  dprdcntz2  20080  dmdprdsplit2lem  20087  ablfacrp  20108  ablfac1eu  20115  pgpfac1lem1  20116  pgpfac1lem2  20117  pgpfac1lem3a  20118  pgpfac1lem3  20119  pgpfac1lem4  20120  pgpfac1lem5  20121  pgpfaclem1  20123  pgpfaclem2  20124  pgpfaclem3  20125  ablfaclem3  20129  ablfac2  20131  prmgrpsimpgd  20156  issubrng2  20608  issubrg2  20642  issubrg3  20650  islss4  21029  dflidl2rng  21288  phssip  21710  mpllsslem  22051  subgtgp  24165  subgntr  24167  opnsubg  24168  clssubg  24169  clsnsg  24170  cldsubg  24171  qustgpopn  24180  qustgphaus  24183  tgptsmscls  24210  subgnm  24693  subgngp  24695  lssnlm  24761  cmscsscms  25435  efgh  26606  efabl  26615  efsubm  26616  subgmulgcld  33223  gsumsubg  33226  qusker  33535  eqgvscpbl  33536  grplsmid  33590  quslsm  33591  qusima  33594  nsgmgc  33598  nsgqusf1olem1  33599  nsgqusf1olem2  33600  nsgqusf1olem3  33601  qsnzr  33642  opprqusplusg  33677  opprqus0g  33678  algextdeglem1  34014  algextdeglem2  34015  algextdeglem3  34016  algextdeglem4  34017  algextdeglem5  34018  nelsubgcld  43119  nelsubgsubcld  43120  idomsubgmo  43770