Theorem subgss 19239

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ⊆ wss 3906  ‘cfv 6540  (class class class)co 7419  Basecbs 17293   ↾_s cress 17314  Grpcgrp 19046  SubGrpcsubg 19232

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7422  df-subg 19235

This theorem is used by:  subgbas  19242  subg0  19244  subginv  19245  subgsubcl  19250  subgsub  19251  subgmulgcl  19252  subgmulg  19253  issubg2  19254  issubg4  19258  subsubg  19262  subgint  19263  trivsubgd  19265  nsgconj  19271  nsgacs  19274  ssnmz  19278  eqger  19292  eqgid  19294  eqgen  19295  eqgcpbl  19296  lagsubg2  19311  lagsubg  19312  eqg0subg  19313  resghm  19348  ghmnsgima  19356  conjsubg  19366  conjsubgen  19367  conjnmz  19368  conjnmzb  19369  gicsubgen  19395  ghmqusnsglem1  19396  ghmquskerlem1  19399  subgga  19416  gasubg  19418  gastacos  19426  orbstafun  19427  cntrsubgnsg  19459  oddvds2  19682  subgpgp  19713  odcau  19720  pgpssslw  19730  sylow2blem1  19736  sylow2blem2  19737  sylow2blem3  19738  slwhash  19740  fislw  19741  sylow2  19742  sylow3lem1  19743  sylow3lem2  19744  sylow3lem3  19745  sylow3lem4  19746  sylow3lem5  19747  sylow3lem6  19748  lsmval  19764  lsmelval  19765  lsmelvali  19766  lsmelvalm  19767  lsmsubg  19770  lsmub1  19773  lsmub2  19774  lsmless1  19776  lsmless2  19777  lsmless12  19778  lsmass  19785  subglsm  19789  lsmmod  19791  cntzrecd  19794  lsmcntz  19795  lsmcntzr  19796  lsmdisj2  19798  subgdisj1  19807  pj1f  19813  pj1id  19815  pj1lid  19817  pj1rid  19818  pj1ghm  19819  qusecsub  19951  subgabl  19952  ablcntzd  19973  lsmcom  19974  dprdff  20130  dprdfadd  20138  dprdres  20146  dprdss  20147  subgdmdprd  20152  dprdcntz2  20156  dmdprdsplit2lem  20163  ablfacrp  20184  ablfac1eu  20191  pgpfac1lem1  20192  pgpfac1lem2  20193  pgpfac1lem3a  20194  pgpfac1lem3  20195  pgpfac1lem4  20196  pgpfac1lem5  20197  pgpfaclem1  20199  pgpfaclem2  20200  pgpfaclem3  20201  ablfaclem3  20205  ablfac2  20207  prmgrpsimpgd  20232  issubrng2  20709  issubrg2  20743  issubrg3  20751  islss4  21135  dflidl2rng  21395  df2idl2crng  21473  qsnzr  21535  phssip  21860  mpllsslem  22201  subgtgp  24315  subgntr  24317  opnsubg  24318  clssubg  24319  clsnsg  24320  cldsubg  24321  qustgpopn  24330  qustgphaus  24333  tgptsmscls  24360  subgnm  24843  subgngp  24845  lssnlm  24911  cmscsscms  25585  efgh  26759  efabl  26768  efsubm  26769  subgmulgcld  33429  gsumsubg  33432  qusker  33735  eqgvscpbl  33736  grplsmid  33779  quslsm  33780  qusima  33783  nsgmgc  33787  nsgqusf1olem1  33788  nsgqusf1olem2  33789  nsgqusf1olem3  33790  opprqusplusg  33837  opprqus0g  33838  algextdeglem1  34173  algextdeglem2  34174  algextdeglem3  34175  algextdeglem4  34176  algextdeglem5  34177  nelsubgcld  43331  nelsubgsubcld  43332  idomsubgmo  43980