Theorem subgss 19094

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ⊆ wss 3883  ‘cfv 6485  (class class class)co 7356  Basecbs 17170   ↾_s cress 17191  Grpcgrp 18900  SubGrpcsubg 19087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fv 6493  df-ov 7359  df-subg 19090

This theorem is referenced by:  subgbas  19097  subg0  19099  subginv  19100  subgsubcl  19104  subgsub  19105  subgmulgcl  19106  subgmulg  19107  issubg2  19108  issubg4  19112  subsubg  19116  subgint  19117  trivsubgd  19119  nsgconj  19125  nsgacs  19128  ssnmz  19132  eqger  19144  eqgid  19146  eqgen  19147  eqgcpbl  19148  lagsubg2  19160  lagsubg  19161  eqg0subg  19162  resghm  19198  ghmnsgima  19206  conjsubg  19216  conjsubgen  19217  conjnmz  19218  conjnmzb  19219  gicsubgen  19245  ghmqusnsglem1  19246  ghmquskerlem1  19249  subgga  19266  gasubg  19268  gastacos  19276  orbstafun  19277  cntrsubgnsg  19309  oddvds2  19532  subgpgp  19563  odcau  19570  pgpssslw  19580  sylow2blem1  19586  sylow2blem2  19587  sylow2blem3  19588  slwhash  19590  fislw  19591  sylow2  19592  sylow3lem1  19593  sylow3lem2  19594  sylow3lem3  19595  sylow3lem4  19596  sylow3lem5  19597  sylow3lem6  19598  lsmval  19614  lsmelval  19615  lsmelvali  19616  lsmelvalm  19617  lsmsubg  19620  lsmub1  19623  lsmub2  19624  lsmless1  19626  lsmless2  19627  lsmless12  19628  lsmass  19635  subglsm  19639  lsmmod  19641  cntzrecd  19644  lsmcntz  19645  lsmcntzr  19646  lsmdisj2  19648  subgdisj1  19657  pj1f  19663  pj1id  19665  pj1lid  19667  pj1rid  19668  pj1ghm  19669  qusecsub  19801  subgabl  19802  ablcntzd  19823  lsmcom  19824  dprdff  19980  dprdfadd  19988  dprdres  19996  dprdss  19997  subgdmdprd  20002  dprdcntz2  20006  dmdprdsplit2lem  20013  ablfacrp  20034  ablfac1eu  20041  pgpfac1lem1  20042  pgpfac1lem2  20043  pgpfac1lem3a  20044  pgpfac1lem3  20045  pgpfac1lem4  20046  pgpfac1lem5  20047  pgpfaclem1  20049  pgpfaclem2  20050  pgpfaclem3  20051  ablfaclem3  20055  ablfac2  20057  prmgrpsimpgd  20082  issubrng2  20530  issubrg2  20564  issubrg3  20572  islss4  20952  dflidl2rng  21211  phssip  21633  mpllsslem  21974  subgtgp  24088  subgntr  24090  opnsubg  24091  clssubg  24092  clsnsg  24093  cldsubg  24094  qustgpopn  24103  qustgphaus  24106  tgptsmscls  24133  subgnm  24616  subgngp  24618  lssnlm  24684  cmscsscms  25358  efgh  26523  efabl  26532  efsubm  26533  subgmulgcld  33124  gsumsubg  33127  qusker  33432  eqgvscpbl  33433  grplsmid  33487  quslsm  33488  qusima  33491  nsgmgc  33495  nsgqusf1olem1  33496  nsgqusf1olem2  33497  nsgqusf1olem3  33498  qsnzr  33538  opprqusplusg  33572  opprqus0g  33573  algextdeglem1  33901  algextdeglem2  33902  algextdeglem3  33903  algextdeglem4  33904  algextdeglem5  33905  nelsubgcld  42987  nelsubgsubcld  42988  idomsubgmo  43638