Theorem subgss 19086

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ⊆ wss 3945  ‘cfv 6547  (class class class)co 7417  Basecbs 17179   ↾_s cress 17208  Grpcgrp 18894  SubGrpcsubg 19079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6499  df-fun 6549  df-fv 6555  df-ov 7420  df-subg 19082

This theorem is referenced by:  subgbas  19089  subg0  19091  subginv  19092  subgsubcl  19096  subgsub  19097  subgmulgcl  19098  subgmulg  19099  issubg2  19100  issubg4  19104  subsubg  19108  subgint  19109  trivsubgd  19112  nsgconj  19118  nsgacs  19121  ssnmz  19125  eqger  19137  eqgid  19139  eqgen  19140  eqgcpbl  19141  lagsubg2  19153  lagsubg  19154  eqg0subg  19155  resghm  19190  ghmnsgima  19198  conjsubg  19208  conjsubgen  19209  conjnmz  19210  conjnmzb  19211  gicsubgen  19237  ghmquskerlem1  19238  subgga  19255  gasubg  19257  gastacos  19265  orbstafun  19266  cntrsubgnsg  19298  oddvds2  19525  subgpgp  19556  odcau  19563  pgpssslw  19573  sylow2blem1  19579  sylow2blem2  19580  sylow2blem3  19581  slwhash  19583  fislw  19584  sylow2  19585  sylow3lem1  19586  sylow3lem2  19587  sylow3lem3  19588  sylow3lem4  19589  sylow3lem5  19590  sylow3lem6  19591  lsmval  19607  lsmelval  19608  lsmelvali  19609  lsmelvalm  19610  lsmsubg  19613  lsmub1  19616  lsmub2  19617  lsmless1  19619  lsmless2  19620  lsmless12  19621  lsmass  19628  subglsm  19632  lsmmod  19634  cntzrecd  19637  lsmcntz  19638  lsmcntzr  19639  lsmdisj2  19641  subgdisj1  19650  pj1f  19656  pj1id  19658  pj1lid  19660  pj1rid  19661  pj1ghm  19662  qusecsub  19794  subgabl  19795  ablcntzd  19816  lsmcom  19817  dprdff  19973  dprdfadd  19981  dprdres  19989  dprdss  19990  subgdmdprd  19995  dprdcntz2  19999  dmdprdsplit2lem  20006  ablfacrp  20027  ablfac1eu  20034  pgpfac1lem1  20035  pgpfac1lem2  20036  pgpfac1lem3a  20037  pgpfac1lem3  20038  pgpfac1lem4  20039  pgpfac1lem5  20040  pgpfaclem1  20042  pgpfaclem2  20043  pgpfaclem3  20044  ablfaclem3  20048  ablfac2  20050  prmgrpsimpgd  20075  issubrng2  20499  issubrg2  20535  issubrg3  20543  islss4  20850  dflidl2rng  21118  phssip  21594  mpllsslem  21949  subgtgp  24039  subgntr  24041  opnsubg  24042  clssubg  24043  clsnsg  24044  cldsubg  24045  qustgpopn  24054  qustgphaus  24057  tgptsmscls  24084  subgnm  24572  subgngp  24574  lssnlm  24648  cmscsscms  25331  efgh  26505  efabl  26514  efsubm  26515  gsumsubg  32817  qusker  33121  eqgvscpbl  33122  grplsmid  33175  quslsm  33177  qusima  33180  nsgmgc  33184  nsgqusf1olem1  33185  nsgqusf1olem2  33186  nsgqusf1olem3  33187  ghmqusnsglem1  33191  qsnzr  33233  opprqusplusg  33262  opprqus0g  33263  algextdeglem1  33455  algextdeglem2  33456  algextdeglem3  33457  algextdeglem4  33458  algextdeglem5  33459  nelsubgcld  41805  nelsubgsubcld  41806  idomsubgmo  42686