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

Theorem subgss 18936
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 18935 . 2 (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆𝐵 ∧ (𝐺s 𝑆) ∈ Grp))
32simp2bi 1147 1 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  wss 3915  cfv 6501  (class class class)co 7362  Basecbs 17090  s cress 17119  Grpcgrp 18755  SubGrpcsubg 18929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fv 6509  df-ov 7365  df-subg 18932
This theorem is referenced by:  subgbas  18939  subg0  18941  subginv  18942  subgsubcl  18946  subgsub  18947  subgmulgcl  18948  subgmulg  18949  issubg2  18950  issubg4  18954  subsubg  18958  subgint  18959  trivsubgd  18962  nsgconj  18968  nsgacs  18971  ssnmz  18975  eqger  18987  eqgid  18989  eqgen  18990  eqgcpbl  18991  lagsubg2  18998  lagsubg  18999  resghm  19031  ghmnsgima  19039  conjsubg  19047  conjsubgen  19048  conjnmz  19049  conjnmzb  19050  gicsubgen  19075  subgga  19087  gasubg  19089  gastacos  19097  orbstafun  19098  cntrsubgnsg  19128  oddvds2  19355  subgpgp  19386  odcau  19393  pgpssslw  19403  sylow2blem1  19409  sylow2blem2  19410  sylow2blem3  19411  slwhash  19413  fislw  19414  sylow2  19415  sylow3lem1  19416  sylow3lem2  19417  sylow3lem3  19418  sylow3lem4  19419  sylow3lem5  19420  sylow3lem6  19421  lsmval  19437  lsmelval  19438  lsmelvali  19439  lsmelvalm  19440  lsmsubg  19443  lsmub1  19446  lsmub2  19447  lsmless1  19449  lsmless2  19450  lsmless12  19451  lsmass  19458  subglsm  19462  lsmmod  19464  cntzrecd  19467  lsmcntz  19468  lsmcntzr  19469  lsmdisj2  19471  subgdisj1  19480  pj1f  19486  pj1id  19488  pj1lid  19490  pj1rid  19491  pj1ghm  19492  subgabl  19621  ablcntzd  19642  lsmcom  19643  dprdff  19798  dprdfadd  19806  dprdres  19814  dprdss  19815  subgdmdprd  19820  dprdcntz2  19824  dmdprdsplit2lem  19831  ablfacrp  19852  ablfac1eu  19859  pgpfac1lem1  19860  pgpfac1lem2  19861  pgpfac1lem3a  19862  pgpfac1lem3  19863  pgpfac1lem4  19864  pgpfac1lem5  19865  pgpfaclem1  19867  pgpfaclem2  19868  pgpfaclem3  19869  ablfaclem3  19873  ablfac2  19875  prmgrpsimpgd  19900  issubrg2  20258  issubrg3  20266  islss4  20439  phssip  21078  mpllsslem  21422  subgtgp  23472  subgntr  23474  opnsubg  23475  clssubg  23476  clsnsg  23477  cldsubg  23478  qustgpopn  23487  qustgphaus  23490  tgptsmscls  23517  subgnm  24005  subgngp  24007  lssnlm  24081  cmscsscms  24753  efgh  25913  efabl  25922  efsubm  25923  gsumsubg  31930  qusker  32181  eqgvscpbl  32182  grplsmid  32225  quslsm  32226  qusima  32227  nsgmgc  32230  nsgqusf1olem1  32231  nsgqusf1olem2  32232  nsgqusf1olem3  32233  ghmquskerlem1  32235  nelsubgcld  40701  nelsubgsubcld  40702  idomsubgmo  41554
  Copyright terms: Public domain W3C validator