Theorem subgss 19337

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  ‘cfv 6538  (class class class)co 7420  Basecbs 17387   ↾_s cress 17408  Grpcgrp 19144  SubGrpcsubg 19330

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-subg 19333

This theorem is used by:  subgbas  19340  subg0  19342  subginv  19343  subgsubcl  19348  subgsub  19349  subgmulgcl  19350  subgmulg  19351  issubg2  19352  issubg4  19356  subsubg  19360  subgint  19361  trivsubgd  19363  nsgconj  19369  nsgacs  19372  ssnmz  19376  eqger  19390  eqgid  19392  eqgen  19393  eqgcpbl  19394  lagsubg2  19409  lagsubg  19410  eqg0subg  19411  resghm  19446  ghmnsgima  19454  conjsubg  19464  conjsubgen  19465  conjnmz  19466  conjnmzb  19467  gicsubgen  19493  ghmqusnsglem1  19494  ghmquskerlem1  19497  subgga  19514  gasubg  19516  gastacos  19524  orbstafun  19525  cntrsubgnsg  19557  oddvds2  19780  subgpgp  19811  odcau  19818  pgpssslw  19828  sylow2blem1  19834  sylow2blem2  19835  sylow2blem3  19836  slwhash  19838  fislw  19839  sylow2  19840  sylow3lem1  19841  sylow3lem2  19842  sylow3lem3  19843  sylow3lem4  19844  sylow3lem5  19845  sylow3lem6  19846  lsmval  19862  lsmelval  19863  lsmelvali  19864  lsmelvalm  19865  lsmsubg  19868  lsmub1  19871  lsmub2  19872  lsmless1  19874  lsmless2  19875  lsmless12  19876  lsmass  19883  subglsm  19887  lsmmod  19889  cntzrecd  19892  lsmcntz  19893  lsmcntzr  19894  lsmdisj2  19896  subgdisj1  19905  pj1f  19911  pj1id  19913  pj1lid  19915  pj1rid  19916  pj1ghm  19917  qusecsub  20049  subgabl  20050  ablcntzd  20071  lsmcom  20072  dprdff  20228  dprdfadd  20236  dprdres  20244  dprdss  20245  subgdmdprd  20250  dprdcntz2  20254  dmdprdsplit2lem  20261  ablfacrp  20282  ablfac1eu  20289  pgpfac1lem1  20290  pgpfac1lem2  20291  pgpfac1lem3a  20292  pgpfac1lem3  20293  pgpfac1lem4  20294  pgpfac1lem5  20295  pgpfaclem1  20297  pgpfaclem2  20298  pgpfaclem3  20299  ablfaclem3  20303  ablfac2  20305  prmgrpsimpgd  20330  issubrng2  20810  issubrg2  20844  issubrg3  20852  islss4  21237  dflidl2rng  21497  df2idl2crng  21577  qsnzr  21639  phssip  21964  mpllsslem  22307  subgtgp  24424  subgntr  24426  opnsubg  24427  clssubg  24428  clsnsg  24429  cldsubg  24430  qustgpopn  24439  qustgphaus  24442  tgptsmscls  24469  subgnm  24952  subgngp  24954  lssnlm  25020  cmscsscms  25694  efgh  26869  efabl  26878  efsubm  26879  subgmulgcld  33604  gsumsubg  33607  qusker  33910  eqgvscpbl  33911  grplsmid  33955  quslsm  33956  qusima  33959  nsgmgc  33963  nsgqusf1olem1  33964  nsgqusf1olem2  33965  nsgqusf1olem3  33966  opprqusplusg  34013  opprqus0g  34014  algextdeglem1  34349  algextdeglem2  34350  algextdeglem3  34351  algextdeglem4  34352  algextdeglem5  34353  nelsubgcld  43561  nelsubgsubcld  43562  idomsubgmo  44194