Theorem subgss 19097

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  ‘cfv 6493  (class class class)co 7361  Basecbs 17173   ↾_s cress 17194  Grpcgrp 18903  SubGrpcsubg 19090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fv 6501  df-ov 7364  df-subg 19093

This theorem is referenced by:  subgbas  19100  subg0  19102  subginv  19103  subgsubcl  19107  subgsub  19108  subgmulgcl  19109  subgmulg  19110  issubg2  19111  issubg4  19115  subsubg  19119  subgint  19120  trivsubgd  19122  nsgconj  19128  nsgacs  19131  ssnmz  19135  eqger  19147  eqgid  19149  eqgen  19150  eqgcpbl  19151  lagsubg2  19163  lagsubg  19164  eqg0subg  19165  resghm  19201  ghmnsgima  19209  conjsubg  19219  conjsubgen  19220  conjnmz  19221  conjnmzb  19222  gicsubgen  19248  ghmqusnsglem1  19249  ghmquskerlem1  19252  subgga  19269  gasubg  19271  gastacos  19279  orbstafun  19280  cntrsubgnsg  19312  oddvds2  19535  subgpgp  19566  odcau  19573  pgpssslw  19583  sylow2blem1  19589  sylow2blem2  19590  sylow2blem3  19591  slwhash  19593  fislw  19594  sylow2  19595  sylow3lem1  19596  sylow3lem2  19597  sylow3lem3  19598  sylow3lem4  19599  sylow3lem5  19600  sylow3lem6  19601  lsmval  19617  lsmelval  19618  lsmelvali  19619  lsmelvalm  19620  lsmsubg  19623  lsmub1  19626  lsmub2  19627  lsmless1  19629  lsmless2  19630  lsmless12  19631  lsmass  19638  subglsm  19642  lsmmod  19644  cntzrecd  19647  lsmcntz  19648  lsmcntzr  19649  lsmdisj2  19651  subgdisj1  19660  pj1f  19666  pj1id  19668  pj1lid  19670  pj1rid  19671  pj1ghm  19672  qusecsub  19804  subgabl  19805  ablcntzd  19826  lsmcom  19827  dprdff  19983  dprdfadd  19991  dprdres  19999  dprdss  20000  subgdmdprd  20005  dprdcntz2  20009  dmdprdsplit2lem  20016  ablfacrp  20037  ablfac1eu  20044  pgpfac1lem1  20045  pgpfac1lem2  20046  pgpfac1lem3a  20047  pgpfac1lem3  20048  pgpfac1lem4  20049  pgpfac1lem5  20050  pgpfaclem1  20052  pgpfaclem2  20053  pgpfaclem3  20054  ablfaclem3  20058  ablfac2  20060  prmgrpsimpgd  20085  issubrng2  20529  issubrg2  20563  issubrg3  20571  islss4  20951  dflidl2rng  21211  phssip  21651  mpllsslem  21991  subgtgp  24083  subgntr  24085  opnsubg  24086  clssubg  24087  clsnsg  24088  cldsubg  24089  qustgpopn  24098  qustgphaus  24101  tgptsmscls  24128  subgnm  24611  subgngp  24613  lssnlm  24679  cmscsscms  25353  efgh  26521  efabl  26530  efsubm  26531  subgmulgcld  33122  gsumsubg  33125  qusker  33427  eqgvscpbl  33428  grplsmid  33482  quslsm  33483  qusima  33486  nsgmgc  33490  nsgqusf1olem1  33491  nsgqusf1olem2  33492  nsgqusf1olem3  33493  qsnzr  33533  opprqusplusg  33567  opprqus0g  33568  algextdeglem1  33880  algextdeglem2  33881  algextdeglem3  33882  algextdeglem4  33883  algextdeglem5  33884  nelsubgcld  42959  nelsubgsubcld  42960  idomsubgmo  43642