Theorem subgss 19253

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 19252	. 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 6533  (class class class)co 7414  Basecbs 17304   ↾_s cress 17325  Grpcgrp 19060  SubGrpcsubg 19246

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7417  df-subg 19249

This theorem is used by:  subgbas  19256  subg0  19258  subginv  19259  subgsubcl  19264  subgsub  19265  subgmulgcl  19266  subgmulg  19267  issubg2  19268  issubg4  19272  subsubg  19276  subgint  19277  trivsubgd  19279  nsgconj  19285  nsgacs  19288  ssnmz  19292  eqger  19306  eqgid  19308  eqgen  19309  eqgcpbl  19310  lagsubg2  19325  lagsubg  19326  eqg0subg  19327  resghm  19362  ghmnsgima  19370  conjsubg  19380  conjsubgen  19381  conjnmz  19382  conjnmzb  19383  gicsubgen  19409  ghmqusnsglem1  19410  ghmquskerlem1  19413  subgga  19430  gasubg  19432  gastacos  19440  orbstafun  19441  cntrsubgnsg  19473  oddvds2  19696  subgpgp  19727  odcau  19734  pgpssslw  19744  sylow2blem1  19750  sylow2blem2  19751  sylow2blem3  19752  slwhash  19754  fislw  19755  sylow2  19756  sylow3lem1  19757  sylow3lem2  19758  sylow3lem3  19759  sylow3lem4  19760  sylow3lem5  19761  sylow3lem6  19762  lsmval  19778  lsmelval  19779  lsmelvali  19780  lsmelvalm  19781  lsmsubg  19784  lsmub1  19787  lsmub2  19788  lsmless1  19790  lsmless2  19791  lsmless12  19792  lsmass  19799  subglsm  19803  lsmmod  19805  cntzrecd  19808  lsmcntz  19809  lsmcntzr  19810  lsmdisj2  19812  subgdisj1  19821  pj1f  19827  pj1id  19829  pj1lid  19831  pj1rid  19832  pj1ghm  19833  qusecsub  19965  subgabl  19966  ablcntzd  19987  lsmcom  19988  dprdff  20144  dprdfadd  20152  dprdres  20160  dprdss  20161  subgdmdprd  20166  dprdcntz2  20170  dmdprdsplit2lem  20177  ablfacrp  20198  ablfac1eu  20205  pgpfac1lem1  20206  pgpfac1lem2  20207  pgpfac1lem3a  20208  pgpfac1lem3  20209  pgpfac1lem4  20210  pgpfac1lem5  20211  pgpfaclem1  20213  pgpfaclem2  20214  pgpfaclem3  20215  ablfaclem3  20219  ablfac2  20221  prmgrpsimpgd  20246  issubrng2  20723  issubrg2  20757  issubrg3  20765  islss4  21149  dflidl2rng  21409  df2idl2crng  21487  qsnzr  21549  phssip  21874  mpllsslem  22217  subgtgp  24334  subgntr  24336  opnsubg  24337  clssubg  24338  clsnsg  24339  cldsubg  24340  qustgpopn  24349  qustgphaus  24352  tgptsmscls  24379  subgnm  24862  subgngp  24864  lssnlm  24930  cmscsscms  25604  efgh  26781  efabl  26790  efsubm  26791  subgmulgcld  33486  gsumsubg  33489  qusker  33792  eqgvscpbl  33793  grplsmid  33836  quslsm  33837  qusima  33840  nsgmgc  33844  nsgqusf1olem1  33845  nsgqusf1olem2  33846  nsgqusf1olem3  33847  opprqusplusg  33894  opprqus0g  33895  algextdeglem1  34230  algextdeglem2  34231  algextdeglem3  34232  algextdeglem4  34233  algextdeglem5  34234  nelsubgcld  43388  nelsubgsubcld  43389  idomsubgmo  44037