Theorem subgss 19073

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099   ⊆ wss 3944  ‘cfv 6542  (class class class)co 7414  Basecbs 17171   ↾_s cress 17200  Grpcgrp 18881  SubGrpcsubg 19066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7417  df-subg 19069

This theorem is referenced by:  subgbas  19076  subg0  19078  subginv  19079  subgsubcl  19083  subgsub  19084  subgmulgcl  19085  subgmulg  19086  issubg2  19087  issubg4  19091  subsubg  19095  subgint  19096  trivsubgd  19099  nsgconj  19105  nsgacs  19108  ssnmz  19112  eqger  19124  eqgid  19126  eqgen  19127  eqgcpbl  19128  lagsubg2  19140  lagsubg  19141  eqg0subg  19142  resghm  19177  ghmnsgima  19185  conjsubg  19195  conjsubgen  19196  conjnmz  19197  conjnmzb  19198  gicsubgen  19224  ghmquskerlem1  19225  subgga  19242  gasubg  19244  gastacos  19252  orbstafun  19253  cntrsubgnsg  19285  oddvds2  19512  subgpgp  19543  odcau  19550  pgpssslw  19560  sylow2blem1  19566  sylow2blem2  19567  sylow2blem3  19568  slwhash  19570  fislw  19571  sylow2  19572  sylow3lem1  19573  sylow3lem2  19574  sylow3lem3  19575  sylow3lem4  19576  sylow3lem5  19577  sylow3lem6  19578  lsmval  19594  lsmelval  19595  lsmelvali  19596  lsmelvalm  19597  lsmsubg  19600  lsmub1  19603  lsmub2  19604  lsmless1  19606  lsmless2  19607  lsmless12  19608  lsmass  19615  subglsm  19619  lsmmod  19621  cntzrecd  19624  lsmcntz  19625  lsmcntzr  19626  lsmdisj2  19628  subgdisj1  19637  pj1f  19643  pj1id  19645  pj1lid  19647  pj1rid  19648  pj1ghm  19649  qusecsub  19781  subgabl  19782  ablcntzd  19803  lsmcom  19804  dprdff  19960  dprdfadd  19968  dprdres  19976  dprdss  19977  subgdmdprd  19982  dprdcntz2  19986  dmdprdsplit2lem  19993  ablfacrp  20014  ablfac1eu  20021  pgpfac1lem1  20022  pgpfac1lem2  20023  pgpfac1lem3a  20024  pgpfac1lem3  20025  pgpfac1lem4  20026  pgpfac1lem5  20027  pgpfaclem1  20029  pgpfaclem2  20030  pgpfaclem3  20031  ablfaclem3  20035  ablfac2  20037  prmgrpsimpgd  20062  issubrng2  20484  issubrg2  20520  issubrg3  20528  islss4  20835  dflidl2rng  21103  phssip  21577  mpllsslem  21929  subgtgp  23996  subgntr  23998  opnsubg  23999  clssubg  24000  clsnsg  24001  cldsubg  24002  qustgpopn  24011  qustgphaus  24014  tgptsmscls  24041  subgnm  24529  subgngp  24531  lssnlm  24605  cmscsscms  25288  efgh  26462  efabl  26471  efsubm  26472  gsumsubg  32738  qusker  33001  eqgvscpbl  33002  grplsmid  33053  quslsm  33055  qusima  33058  nsgmgc  33062  nsgqusf1olem1  33063  nsgqusf1olem2  33064  nsgqusf1olem3  33065  qsnzr  33107  opprqusplusg  33136  opprqus0g  33137  algextdeglem1  33321  algextdeglem2  33322  algextdeglem3  33323  algextdeglem4  33324  algextdeglem5  33325  nelsubgcld  41657  nelsubgsubcld  41658  idomsubgmo  42543