Theorem subgss 19349

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146   ⊆ wss 3899  ‘cfv 6546  (class class class)co 7427  Basecbs 17399   ↾_s cress 17420  Grpcgrp 19156  SubGrpcsubg 19342

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  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 6500  df-fun 6548  df-fv 6554  df-ov 7430  df-subg 19345

This theorem is used by:  subgbas  19352  subg0  19354  subginv  19355  subgsubcl  19360  subgsub  19361  subgmulgcl  19362  subgmulg  19363  issubg2  19364  issubg4  19368  subsubg  19372  subgint  19373  trivsubgd  19375  nsgconj  19381  nsgacs  19384  ssnmz  19388  eqger  19402  eqgid  19404  eqgen  19405  eqgcpbl  19406  lagsubg2  19421  lagsubg  19422  eqg0subg  19423  resghm  19458  ghmnsgima  19466  conjsubg  19476  conjsubgen  19477  conjnmz  19478  conjnmzb  19479  gicsubgen  19505  ghmqusnsglem1  19506  ghmquskerlem1  19509  subgga  19526  gasubg  19528  gastacos  19536  orbstafun  19537  cntrsubgnsg  19569  oddvds2  19792  subgpgp  19823  odcau  19830  pgpssslw  19840  sylow2blem1  19846  sylow2blem2  19847  sylow2blem3  19848  slwhash  19850  fislw  19851  sylow2  19852  sylow3lem1  19853  sylow3lem2  19854  sylow3lem3  19855  sylow3lem4  19856  sylow3lem5  19857  sylow3lem6  19858  lsmval  19874  lsmelval  19875  lsmelvali  19876  lsmelvalm  19877  lsmsubg  19880  lsmub1  19883  lsmub2  19884  lsmless1  19886  lsmless2  19887  lsmless12  19888  lsmass  19895  subglsm  19899  lsmmod  19901  cntzrecd  19904  lsmcntz  19905  lsmcntzr  19906  lsmdisj2  19908  subgdisj1  19917  pj1f  19923  pj1id  19925  pj1lid  19927  pj1rid  19928  pj1ghm  19929  qusecsub  20061  subgabl  20062  ablcntzd  20083  lsmcom  20084  dprdff  20240  dprdfadd  20248  dprdres  20256  dprdss  20257  subgdmdprd  20262  dprdcntz2  20266  dmdprdsplit2lem  20273  ablfacrp  20294  ablfac1eu  20301  pgpfac1lem1  20302  pgpfac1lem2  20303  pgpfac1lem3a  20304  pgpfac1lem3  20305  pgpfac1lem4  20306  pgpfac1lem5  20307  pgpfaclem1  20309  pgpfaclem2  20310  pgpfaclem3  20311  ablfaclem3  20315  ablfac2  20317  prmgrpsimpgd  20342  issubrng2  20822  issubrg2  20856  issubrg3  20864  islss4  21249  dflidl2rng  21509  df2idl2crng  21589  qsnzr  21651  phssip  21976  mpllsslem  22319  subgtgp  24436  subgntr  24438  opnsubg  24439  clssubg  24440  clsnsg  24441  cldsubg  24442  qustgpopn  24451  qustgphaus  24454  tgptsmscls  24481  subgnm  24964  subgngp  24966  lssnlm  25032  cmscsscms  25706  efgh  26881  efabl  26890  efsubm  26891  subgmulgcld  33657  gsumsubg  33660  qusker  33963  eqgvscpbl  33964  grplsmid  34008  quslsm  34009  qusima  34012  nsgmgc  34016  nsgqusf1olem1  34017  nsgqusf1olem2  34018  nsgqusf1olem3  34019  opprqusplusg  34066  opprqus0g  34067  algextdeglem1  34402  algextdeglem2  34403  algextdeglem3  34404  algextdeglem4  34405  algextdeglem5  34406  nelsubgcld  43701  nelsubgsubcld  43702  idomsubgmo  44335