MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subgss Structured version   Visualization version   GIF version

Theorem subgss 18278
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
StepHypRef Expression
1 issubg.b . . 3 𝐵 = (Base‘𝐺)
21issubg 18277 . 2 (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆𝐵 ∧ (𝐺s 𝑆) ∈ Grp))
32simp2bi 1143 1 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  wss 3919  cfv 6344  (class class class)co 7146  Basecbs 16481  s cress 16482  Grpcgrp 18101  SubGrpcsubg 18271
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4826  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-iota 6303  df-fun 6346  df-fv 6352  df-ov 7149  df-subg 18274
This theorem is referenced by:  subgbas  18281  subg0  18283  subginv  18284  subgsubcl  18288  subgsub  18289  subgmulgcl  18290  subgmulg  18291  issubg2  18292  issubg4  18296  subsubg  18300  subgint  18301  trivsubgd  18303  nsgconj  18309  nsgacs  18312  ssnmz  18316  eqger  18328  eqgid  18330  eqgen  18331  eqgcpbl  18332  lagsubg2  18339  lagsubg  18340  resghm  18372  ghmnsgima  18380  conjsubg  18388  conjsubgen  18389  conjnmz  18390  conjnmzb  18391  gicsubgen  18416  subgga  18428  gasubg  18430  gastacos  18438  orbstafun  18439  cntrsubgnsg  18469  oddvds2  18691  subgpgp  18720  odcau  18727  pgpssslw  18737  sylow2blem1  18743  sylow2blem2  18744  sylow2blem3  18745  slwhash  18747  fislw  18748  sylow2  18749  sylow3lem1  18750  sylow3lem2  18751  sylow3lem3  18752  sylow3lem4  18753  sylow3lem5  18754  sylow3lem6  18755  lsmval  18771  lsmelval  18772  lsmelvali  18773  lsmelvalm  18774  lsmsubg  18777  lsmub1  18780  lsmub2  18781  lsmless1  18783  lsmless2  18784  lsmless12  18785  lsmass  18793  subglsm  18797  lsmmod  18799  cntzrecd  18802  lsmcntz  18803  lsmcntzr  18804  lsmdisj2  18806  subgdisj1  18815  pj1f  18821  pj1id  18823  pj1lid  18825  pj1rid  18826  pj1ghm  18827  subgabl  18954  ablcntzd  18975  lsmcom  18976  dprdff  19132  dprdfadd  19140  dprdres  19148  dprdss  19149  subgdmdprd  19154  dprdcntz2  19158  dmdprdsplit2lem  19165  ablfacrp  19186  ablfac1eu  19193  pgpfac1lem1  19194  pgpfac1lem2  19195  pgpfac1lem3a  19196  pgpfac1lem3  19197  pgpfac1lem4  19198  pgpfac1lem5  19199  pgpfaclem1  19201  pgpfaclem2  19202  pgpfaclem3  19203  ablfaclem3  19207  ablfac2  19209  prmgrpsimpgd  19234  issubrg2  19550  issubrg3  19558  islss4  19729  mpllsslem  20210  phssip  20797  subgtgp  22708  subgntr  22710  opnsubg  22711  clssubg  22712  clsnsg  22713  cldsubg  22714  qustgpopn  22723  qustgphaus  22726  tgptsmscls  22753  subgnm  23237  subgngp  23239  lssnlm  23305  cmscsscms  23975  efgh  25131  efabl  25140  efsubm  25141  gsumsubg  30711  qusker  30945  eqgvscpbl  30946  nelsubgcld  39303  nelsubgsubcld  39304  idomsubgmo  39998
  Copyright terms: Public domain W3C validator