Theorem subgss 17516

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

Syntax hints:   → wi 4   = wceq 1480   ∈ wcel 1987   ⊆ wss 3555  ‘cfv 5847  (class class class)co 6604  Basecbs 15781   ↾_s cress 15782  Grpcgrp 17343  SubGrpcsubg 17509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fv 5855  df-ov 6607  df-subg 17512

This theorem is referenced by:  subgbas  17519  subg0  17521  subginv  17522  subgsubcl  17526  subgsub  17527  subgmulgcl  17528  subgmulg  17529  issubg2  17530  issubg4  17534  subsubg  17538  subgint  17539  nsgconj  17548  nsgacs  17551  ssnmz  17557  eqger  17565  eqgid  17567  eqgen  17568  eqgcpbl  17569  lagsubg2  17576  lagsubg  17577  resghm  17597  ghmnsgima  17605  conjsubg  17613  conjsubgen  17614  conjnmz  17615  conjnmzb  17616  gicsubgen  17642  subgga  17654  gasubg  17656  gastacos  17664  orbstafun  17665  cntrsubgnsg  17694  oddvds2  17904  subgpgp  17933  odcau  17940  pgpssslw  17950  sylow2blem1  17956  sylow2blem2  17957  sylow2blem3  17958  slwhash  17960  fislw  17961  sylow2  17962  sylow3lem1  17963  sylow3lem2  17964  sylow3lem3  17965  sylow3lem4  17966  sylow3lem5  17967  sylow3lem6  17968  lsmval  17984  lsmelval  17985  lsmelvali  17986  lsmelvalm  17987  lsmsubg  17990  lsmub1  17992  lsmub2  17993  lsmless1  17995  lsmless2  17996  lsmless12  17997  lsmass  18004  subglsm  18007  lsmmod  18009  cntzrecd  18012  lsmcntz  18013  lsmcntzr  18014  lsmdisj2  18016  subgdisj1  18025  pj1f  18031  pj1id  18033  pj1lid  18035  pj1rid  18036  pj1ghm  18037  subgabl  18162  ablcntzd  18181  lsmcom  18182  dprdff  18332  dprdfadd  18340  dprdres  18348  dprdss  18349  subgdmdprd  18354  dprdcntz2  18358  dmdprdsplit2lem  18365  ablfacrp  18386  ablfac1eu  18393  pgpfac1lem1  18394  pgpfac1lem2  18395  pgpfac1lem3a  18396  pgpfac1lem3  18397  pgpfac1lem4  18398  pgpfac1lem5  18399  pgpfaclem1  18401  pgpfaclem2  18402  pgpfaclem3  18403  ablfaclem3  18407  ablfac2  18409  issubrg2  18721  issubrg3  18729  islss4  18881  mpllsslem  19354  phssip  19922  subgtgp  21819  subgntr  21820  opnsubg  21821  clssubg  21822  clsnsg  21823  cldsubg  21824  qustgpopn  21833  qustgphaus  21836  tgptsmscls  21863  subgnm  22347  subgngp  22349  lssnlm  22415  efgh  24191  efabl  24200  efsubm  24201  idomsubgmo  37254