Theorem subgss 17796

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

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139   ⊆ wss 3715  ‘cfv 6049  (class class class)co 6813  Basecbs 16059   ↾_s cress 16060  Grpcgrp 17623  SubGrpcsubg 17789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fv 6057  df-ov 6816  df-subg 17792

This theorem is referenced by:  subgbas  17799  subg0  17801  subginv  17802  subgsubcl  17806  subgsub  17807  subgmulgcl  17808  subgmulg  17809  issubg2  17810  issubg4  17814  subsubg  17818  subgint  17819  nsgconj  17828  nsgacs  17831  ssnmz  17837  eqger  17845  eqgid  17847  eqgen  17848  eqgcpbl  17849  lagsubg2  17856  lagsubg  17857  resghm  17877  ghmnsgima  17885  conjsubg  17893  conjsubgen  17894  conjnmz  17895  conjnmzb  17896  gicsubgen  17921  subgga  17933  gasubg  17935  gastacos  17943  orbstafun  17944  cntrsubgnsg  17973  oddvds2  18183  subgpgp  18212  odcau  18219  pgpssslw  18229  sylow2blem1  18235  sylow2blem2  18236  sylow2blem3  18237  slwhash  18239  fislw  18240  sylow2  18241  sylow3lem1  18242  sylow3lem2  18243  sylow3lem3  18244  sylow3lem4  18245  sylow3lem5  18246  sylow3lem6  18247  lsmval  18263  lsmelval  18264  lsmelvali  18265  lsmelvalm  18266  lsmsubg  18269  lsmub1  18271  lsmub2  18272  lsmless1  18274  lsmless2  18275  lsmless12  18276  lsmass  18283  subglsm  18286  lsmmod  18288  cntzrecd  18291  lsmcntz  18292  lsmcntzr  18293  lsmdisj2  18295  subgdisj1  18304  pj1f  18310  pj1id  18312  pj1lid  18314  pj1rid  18315  pj1ghm  18316  subgabl  18441  ablcntzd  18460  lsmcom  18461  dprdff  18611  dprdfadd  18619  dprdres  18627  dprdss  18628  subgdmdprd  18633  dprdcntz2  18637  dmdprdsplit2lem  18644  ablfacrp  18665  ablfac1eu  18672  pgpfac1lem1  18673  pgpfac1lem2  18674  pgpfac1lem3a  18675  pgpfac1lem3  18676  pgpfac1lem4  18677  pgpfac1lem5  18678  pgpfaclem1  18680  pgpfaclem2  18681  pgpfaclem3  18682  ablfaclem3  18686  ablfac2  18688  issubrg2  19002  issubrg3  19010  islss4  19164  mpllsslem  19637  phssip  20205  subgtgp  22110  subgntr  22111  opnsubg  22112  clssubg  22113  clsnsg  22114  cldsubg  22115  qustgpopn  22124  qustgphaus  22127  tgptsmscls  22154  subgnm  22638  subgngp  22640  lssnlm  22706  efgh  24486  efabl  24495  efsubm  24496  idomsubgmo  38278