Theorem subgss 19041

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ⊆ wss 3911  ‘cfv 6499  (class class class)co 7369  Basecbs 17155   ↾_s cress 17176  Grpcgrp 18847  SubGrpcsubg 19034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fv 6507  df-ov 7372  df-subg 19037

This theorem is referenced by:  subgbas  19044  subg0  19046  subginv  19047  subgsubcl  19051  subgsub  19052  subgmulgcl  19053  subgmulg  19054  issubg2  19055  issubg4  19059  subsubg  19063  subgint  19064  trivsubgd  19067  nsgconj  19073  nsgacs  19076  ssnmz  19080  eqger  19092  eqgid  19094  eqgen  19095  eqgcpbl  19096  lagsubg2  19108  lagsubg  19109  eqg0subg  19110  resghm  19146  ghmnsgima  19154  conjsubg  19164  conjsubgen  19165  conjnmz  19166  conjnmzb  19167  gicsubgen  19193  ghmqusnsglem1  19194  ghmquskerlem1  19197  subgga  19214  gasubg  19216  gastacos  19224  orbstafun  19225  cntrsubgnsg  19257  oddvds2  19480  subgpgp  19511  odcau  19518  pgpssslw  19528  sylow2blem1  19534  sylow2blem2  19535  sylow2blem3  19536  slwhash  19538  fislw  19539  sylow2  19540  sylow3lem1  19541  sylow3lem2  19542  sylow3lem3  19543  sylow3lem4  19544  sylow3lem5  19545  sylow3lem6  19546  lsmval  19562  lsmelval  19563  lsmelvali  19564  lsmelvalm  19565  lsmsubg  19568  lsmub1  19571  lsmub2  19572  lsmless1  19574  lsmless2  19575  lsmless12  19576  lsmass  19583  subglsm  19587  lsmmod  19589  cntzrecd  19592  lsmcntz  19593  lsmcntzr  19594  lsmdisj2  19596  subgdisj1  19605  pj1f  19611  pj1id  19613  pj1lid  19615  pj1rid  19616  pj1ghm  19617  qusecsub  19749  subgabl  19750  ablcntzd  19771  lsmcom  19772  dprdff  19928  dprdfadd  19936  dprdres  19944  dprdss  19945  subgdmdprd  19950  dprdcntz2  19954  dmdprdsplit2lem  19961  ablfacrp  19982  ablfac1eu  19989  pgpfac1lem1  19990  pgpfac1lem2  19991  pgpfac1lem3a  19992  pgpfac1lem3  19993  pgpfac1lem4  19994  pgpfac1lem5  19995  pgpfaclem1  19997  pgpfaclem2  19998  pgpfaclem3  19999  ablfaclem3  20003  ablfac2  20005  prmgrpsimpgd  20030  issubrng2  20478  issubrg2  20512  issubrg3  20520  islss4  20900  dflidl2rng  21160  phssip  21600  mpllsslem  21942  subgtgp  24025  subgntr  24027  opnsubg  24028  clssubg  24029  clsnsg  24030  cldsubg  24031  qustgpopn  24040  qustgphaus  24043  tgptsmscls  24070  subgnm  24554  subgngp  24556  lssnlm  24622  cmscsscms  25306  efgh  26483  efabl  26492  efsubm  26493  subgmulgcld  33027  gsumsubg  33029  qusker  33313  eqgvscpbl  33314  grplsmid  33368  quslsm  33369  qusima  33372  nsgmgc  33376  nsgqusf1olem1  33377  nsgqusf1olem2  33378  nsgqusf1olem3  33379  qsnzr  33419  opprqusplusg  33453  opprqus0g  33454  algextdeglem1  33700  algextdeglem2  33701  algextdeglem3  33702  algextdeglem4  33703  algextdeglem5  33704  nelsubgcld  42478  nelsubgsubcld  42479  idomsubgmo  43175