Theorem subgss 19110

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ⊆ wss 3926  ‘cfv 6531  (class class class)co 7405  Basecbs 17228   ↾_s cress 17251  Grpcgrp 18916  SubGrpcsubg 19103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-subg 19106

This theorem is referenced by:  subgbas  19113  subg0  19115  subginv  19116  subgsubcl  19120  subgsub  19121  subgmulgcl  19122  subgmulg  19123  issubg2  19124  issubg4  19128  subsubg  19132  subgint  19133  trivsubgd  19136  nsgconj  19142  nsgacs  19145  ssnmz  19149  eqger  19161  eqgid  19163  eqgen  19164  eqgcpbl  19165  lagsubg2  19177  lagsubg  19178  eqg0subg  19179  resghm  19215  ghmnsgima  19223  conjsubg  19233  conjsubgen  19234  conjnmz  19235  conjnmzb  19236  gicsubgen  19262  ghmqusnsglem1  19263  ghmquskerlem1  19266  subgga  19283  gasubg  19285  gastacos  19293  orbstafun  19294  cntrsubgnsg  19326  oddvds2  19547  subgpgp  19578  odcau  19585  pgpssslw  19595  sylow2blem1  19601  sylow2blem2  19602  sylow2blem3  19603  slwhash  19605  fislw  19606  sylow2  19607  sylow3lem1  19608  sylow3lem2  19609  sylow3lem3  19610  sylow3lem4  19611  sylow3lem5  19612  sylow3lem6  19613  lsmval  19629  lsmelval  19630  lsmelvali  19631  lsmelvalm  19632  lsmsubg  19635  lsmub1  19638  lsmub2  19639  lsmless1  19641  lsmless2  19642  lsmless12  19643  lsmass  19650  subglsm  19654  lsmmod  19656  cntzrecd  19659  lsmcntz  19660  lsmcntzr  19661  lsmdisj2  19663  subgdisj1  19672  pj1f  19678  pj1id  19680  pj1lid  19682  pj1rid  19683  pj1ghm  19684  qusecsub  19816  subgabl  19817  ablcntzd  19838  lsmcom  19839  dprdff  19995  dprdfadd  20003  dprdres  20011  dprdss  20012  subgdmdprd  20017  dprdcntz2  20021  dmdprdsplit2lem  20028  ablfacrp  20049  ablfac1eu  20056  pgpfac1lem1  20057  pgpfac1lem2  20058  pgpfac1lem3a  20059  pgpfac1lem3  20060  pgpfac1lem4  20061  pgpfac1lem5  20062  pgpfaclem1  20064  pgpfaclem2  20065  pgpfaclem3  20066  ablfaclem3  20070  ablfac2  20072  prmgrpsimpgd  20097  issubrng2  20518  issubrg2  20552  issubrg3  20560  islss4  20919  dflidl2rng  21179  phssip  21618  mpllsslem  21960  subgtgp  24043  subgntr  24045  opnsubg  24046  clssubg  24047  clsnsg  24048  cldsubg  24049  qustgpopn  24058  qustgphaus  24061  tgptsmscls  24088  subgnm  24572  subgngp  24574  lssnlm  24640  cmscsscms  25325  efgh  26502  efabl  26511  efsubm  26512  subgmulgcld  33038  gsumsubg  33040  qusker  33364  eqgvscpbl  33365  grplsmid  33419  quslsm  33420  qusima  33423  nsgmgc  33427  nsgqusf1olem1  33428  nsgqusf1olem2  33429  nsgqusf1olem3  33430  qsnzr  33470  opprqusplusg  33504  opprqus0g  33505  algextdeglem1  33751  algextdeglem2  33752  algextdeglem3  33753  algextdeglem4  33754  algextdeglem5  33755  nelsubgcld  42520  nelsubgsubcld  42521  idomsubgmo  43217