Theorem subgss 19055

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ⊆ wss 3899  ‘cfv 6490  (class class class)co 7356  Basecbs 17134   ↾_s cress 17155  Grpcgrp 18861  SubGrpcsubg 19048

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fv 6498  df-ov 7359  df-subg 19051

This theorem is referenced by:  subgbas  19058  subg0  19060  subginv  19061  subgsubcl  19065  subgsub  19066  subgmulgcl  19067  subgmulg  19068  issubg2  19069  issubg4  19073  subsubg  19077  subgint  19078  trivsubgd  19080  nsgconj  19086  nsgacs  19089  ssnmz  19093  eqger  19105  eqgid  19107  eqgen  19108  eqgcpbl  19109  lagsubg2  19121  lagsubg  19122  eqg0subg  19123  resghm  19159  ghmnsgima  19167  conjsubg  19177  conjsubgen  19178  conjnmz  19179  conjnmzb  19180  gicsubgen  19206  ghmqusnsglem1  19207  ghmquskerlem1  19210  subgga  19227  gasubg  19229  gastacos  19237  orbstafun  19238  cntrsubgnsg  19270  oddvds2  19493  subgpgp  19524  odcau  19531  pgpssslw  19541  sylow2blem1  19547  sylow2blem2  19548  sylow2blem3  19549  slwhash  19551  fislw  19552  sylow2  19553  sylow3lem1  19554  sylow3lem2  19555  sylow3lem3  19556  sylow3lem4  19557  sylow3lem5  19558  sylow3lem6  19559  lsmval  19575  lsmelval  19576  lsmelvali  19577  lsmelvalm  19578  lsmsubg  19581  lsmub1  19584  lsmub2  19585  lsmless1  19587  lsmless2  19588  lsmless12  19589  lsmass  19596  subglsm  19600  lsmmod  19602  cntzrecd  19605  lsmcntz  19606  lsmcntzr  19607  lsmdisj2  19609  subgdisj1  19618  pj1f  19624  pj1id  19626  pj1lid  19628  pj1rid  19629  pj1ghm  19630  qusecsub  19762  subgabl  19763  ablcntzd  19784  lsmcom  19785  dprdff  19941  dprdfadd  19949  dprdres  19957  dprdss  19958  subgdmdprd  19963  dprdcntz2  19967  dmdprdsplit2lem  19974  ablfacrp  19995  ablfac1eu  20002  pgpfac1lem1  20003  pgpfac1lem2  20004  pgpfac1lem3a  20005  pgpfac1lem3  20006  pgpfac1lem4  20007  pgpfac1lem5  20008  pgpfaclem1  20010  pgpfaclem2  20011  pgpfaclem3  20012  ablfaclem3  20016  ablfac2  20018  prmgrpsimpgd  20043  issubrng2  20489  issubrg2  20523  issubrg3  20531  islss4  20911  dflidl2rng  21171  phssip  21611  mpllsslem  21953  subgtgp  24047  subgntr  24049  opnsubg  24050  clssubg  24051  clsnsg  24052  cldsubg  24053  qustgpopn  24062  qustgphaus  24065  tgptsmscls  24092  subgnm  24575  subgngp  24577  lssnlm  24643  cmscsscms  25327  efgh  26504  efabl  26513  efsubm  26514  subgmulgcld  33075  gsumsubg  33078  qusker  33379  eqgvscpbl  33380  grplsmid  33434  quslsm  33435  qusima  33438  nsgmgc  33442  nsgqusf1olem1  33443  nsgqusf1olem2  33444  nsgqusf1olem3  33445  qsnzr  33485  opprqusplusg  33519  opprqus0g  33520  algextdeglem1  33823  algextdeglem2  33824  algextdeglem3  33825  algextdeglem4  33826  algextdeglem5  33827  nelsubgcld  42694  nelsubgsubcld  42695  idomsubgmo  43377