Theorem subgss 17792

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

Syntax hints:   → wi 4   = wceq 1628   ∈ wcel 2135   ⊆ wss 3711  ‘cfv 6045  (class class class)co 6809  Basecbs 16055   ↾_s cress 16056  Grpcgrp 17619  SubGrpcsubg 17785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-sbc 3573  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fv 6053  df-ov 6812  df-subg 17788

This theorem is referenced by:  subgbas  17795  subg0  17797  subginv  17798  subgsubcl  17802  subgsub  17803  subgmulgcl  17804  subgmulg  17805  issubg2  17806  issubg4  17810  subsubg  17814  subgint  17815  nsgconj  17824  nsgacs  17827  ssnmz  17833  eqger  17841  eqgid  17843  eqgen  17844  eqgcpbl  17845  lagsubg2  17852  lagsubg  17853  resghm  17873  ghmnsgima  17881  conjsubg  17889  conjsubgen  17890  conjnmz  17891  conjnmzb  17892  gicsubgen  17917  subgga  17929  gasubg  17931  gastacos  17939  orbstafun  17940  cntrsubgnsg  17969  oddvds2  18179  subgpgp  18208  odcau  18215  pgpssslw  18225  sylow2blem1  18231  sylow2blem2  18232  sylow2blem3  18233  slwhash  18235  fislw  18236  sylow2  18237  sylow3lem1  18238  sylow3lem2  18239  sylow3lem3  18240  sylow3lem4  18241  sylow3lem5  18242  sylow3lem6  18243  lsmval  18259  lsmelval  18260  lsmelvali  18261  lsmelvalm  18262  lsmsubg  18265  lsmub1  18267  lsmub2  18268  lsmless1  18270  lsmless2  18271  lsmless12  18272  lsmass  18279  subglsm  18282  lsmmod  18284  cntzrecd  18287  lsmcntz  18288  lsmcntzr  18289  lsmdisj2  18291  subgdisj1  18300  pj1f  18306  pj1id  18308  pj1lid  18310  pj1rid  18311  pj1ghm  18312  subgabl  18437  ablcntzd  18456  lsmcom  18457  dprdff  18607  dprdfadd  18615  dprdres  18623  dprdss  18624  subgdmdprd  18629  dprdcntz2  18633  dmdprdsplit2lem  18640  ablfacrp  18661  ablfac1eu  18668  pgpfac1lem1  18669  pgpfac1lem2  18670  pgpfac1lem3a  18671  pgpfac1lem3  18672  pgpfac1lem4  18673  pgpfac1lem5  18674  pgpfaclem1  18676  pgpfaclem2  18677  pgpfaclem3  18678  ablfaclem3  18682  ablfac2  18684  issubrg2  18998  issubrg3  19006  islss4  19160  mpllsslem  19633  phssip  20201  subgtgp  22106  subgntr  22107  opnsubg  22108  clssubg  22109  clsnsg  22110  cldsubg  22111  qustgpopn  22120  qustgphaus  22123  tgptsmscls  22150  subgnm  22634  subgngp  22636  lssnlm  22702  efgh  24482  efabl  24491  efsubm  24492  idomsubgmo  38274