Theorem subgss 19387

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900  ‘cfv 6566  (class class class)co 7451  Basecbs 17431   ↾_s cress 17452  Grpcgrp 19194  SubGrpcsubg 19380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fv 6574  df-ov 7454  df-subg 19383

This theorem is used by:  subgbas  19390  subg0  19392  subginv  19393  subgsubcl  19398  subgsub  19399  subgmulgcl  19400  subgmulg  19401  issubg2  19402  issubg4  19406  subsubg  19410  subgint  19411  trivsubgd  19413  nsgconj  19419  nsgacs  19422  ssnmz  19426  eqger  19440  eqgid  19442  eqgen  19443  eqgcpbl  19444  lagsubg2  19459  lagsubg  19460  eqg0subg  19461  resghm  19496  ghmnsgima  19504  conjsubg  19514  conjsubgen  19515  conjnmz  19516  conjnmzb  19517  gicsubgen  19544  ghmqusnsglem1  19545  ghmquskerlem1  19548  subgga  19565  gasubg  19567  gastacos  19575  orbstafun  19576  cntrsubgnsg  19608  oddvds2  19831  subgpgp  19862  odcau  19869  pgpssslw  19879  sylow2blem1  19885  sylow2blem2  19886  sylow2blem3  19887  slwhash  19889  fislw  19890  sylow2  19891  sylow3lem1  19892  sylow3lem2  19893  sylow3lem3  19894  sylow3lem4  19895  sylow3lem5  19896  sylow3lem6  19897  lsmval  19913  lsmelval  19914  lsmelvali  19915  lsmelvalm  19916  lsmsubg  19919  lsmub1  19922  lsmub2  19923  lsmless1  19925  lsmless2  19926  lsmless12  19927  lsmass  19934  subglsm  19938  lsmmod  19940  cntzrecd  19943  lsmcntz  19944  lsmcntzr  19945  lsmdisj2  19947  subgdisj1  19956  pj1f  19962  pj1id  19964  pj1lid  19966  pj1rid  19967  pj1ghm  19968  qusecsub  20100  subgabl  20101  ablcntzd  20122  lsmcom  20123  dprdff  20279  dprdfadd  20287  dprdres  20295  dprdss  20296  subgdmdprd  20301  dprdcntz2  20305  dmdprdsplit2lem  20312  ablfacrp  20333  ablfac1eu  20340  pgpfac1lem1  20341  pgpfac1lem2  20342  pgpfac1lem3a  20343  pgpfac1lem3  20344  pgpfac1lem4  20345  pgpfac1lem5  20346  pgpfaclem1  20348  pgpfaclem2  20349  pgpfaclem3  20350  ablfaclem3  20354  ablfac2  20356  prmgrpsimpgd  20381  issubrng2  20861  issubrg2  20895  issubrg3  20903  islss4  21288  dflidl2rng  21548  df2idl2crng  21628  qsnzr  21690  phssip  22019  mpllsslem  22362  subgtgp  24479  subgntr  24481  opnsubg  24482  clssubg  24483  clsnsg  24484  cldsubg  24485  qustgpopn  24494  qustgphaus  24497  tgptsmscls  24524  subgnm  25007  subgngp  25009  lssnlm  25075  cmscsscms  25749  efgh  26926  efabl  26935  efsubm  26936  subgmulgcld  33703  gsumsubg  33706  qusker  34014  eqgvscpbl  34015  grplsmid  34059  quslsm  34060  qusima  34063  nsgmgc  34067  nsgqusf1olem1  34068  nsgqusf1olem2  34069  nsgqusf1olem3  34070  opprqusplusg  34117  opprqus0g  34118  algextdeglem1  34460  algextdeglem2  34461  algextdeglem3  34462  algextdeglem4  34463  algextdeglem5  34464  nelsubgcld  43827  nelsubgsubcld  43828  idomsubgmo  44456