Theorem subgss 19162

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2103   ⊆ wss 3970  ‘cfv 6572  (class class class)co 7445  Basecbs 17253   ↾_s cress 17282  Grpcgrp 18968  SubGrpcsubg 19155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pow 5386  ax-pr 5450

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3439  df-v 3484  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fv 6580  df-ov 7448  df-subg 19158

This theorem is referenced by:  subgbas  19165  subg0  19167  subginv  19168  subgsubcl  19172  subgsub  19173  subgmulgcl  19174  subgmulg  19175  issubg2  19176  issubg4  19180  subsubg  19184  subgint  19185  trivsubgd  19188  nsgconj  19194  nsgacs  19197  ssnmz  19201  eqger  19213  eqgid  19215  eqgen  19216  eqgcpbl  19217  lagsubg2  19229  lagsubg  19230  eqg0subg  19231  resghm  19267  ghmnsgima  19275  conjsubg  19285  conjsubgen  19286  conjnmz  19287  conjnmzb  19288  gicsubgen  19314  ghmqusnsglem1  19315  ghmquskerlem1  19318  subgga  19335  gasubg  19337  gastacos  19345  orbstafun  19346  cntrsubgnsg  19378  oddvds2  19603  subgpgp  19634  odcau  19641  pgpssslw  19651  sylow2blem1  19657  sylow2blem2  19658  sylow2blem3  19659  slwhash  19661  fislw  19662  sylow2  19663  sylow3lem1  19664  sylow3lem2  19665  sylow3lem3  19666  sylow3lem4  19667  sylow3lem5  19668  sylow3lem6  19669  lsmval  19685  lsmelval  19686  lsmelvali  19687  lsmelvalm  19688  lsmsubg  19691  lsmub1  19694  lsmub2  19695  lsmless1  19697  lsmless2  19698  lsmless12  19699  lsmass  19706  subglsm  19710  lsmmod  19712  cntzrecd  19715  lsmcntz  19716  lsmcntzr  19717  lsmdisj2  19719  subgdisj1  19728  pj1f  19734  pj1id  19736  pj1lid  19738  pj1rid  19739  pj1ghm  19740  qusecsub  19872  subgabl  19873  ablcntzd  19894  lsmcom  19895  dprdff  20051  dprdfadd  20059  dprdres  20067  dprdss  20068  subgdmdprd  20073  dprdcntz2  20077  dmdprdsplit2lem  20084  ablfacrp  20105  ablfac1eu  20112  pgpfac1lem1  20113  pgpfac1lem2  20114  pgpfac1lem3a  20115  pgpfac1lem3  20116  pgpfac1lem4  20117  pgpfac1lem5  20118  pgpfaclem1  20120  pgpfaclem2  20121  pgpfaclem3  20122  ablfaclem3  20126  ablfac2  20128  prmgrpsimpgd  20153  issubrng2  20579  issubrg2  20615  issubrg3  20623  islss4  20978  dflidl2rng  21246  phssip  21694  mpllsslem  22037  subgtgp  24127  subgntr  24129  opnsubg  24130  clssubg  24131  clsnsg  24132  cldsubg  24133  qustgpopn  24142  qustgphaus  24145  tgptsmscls  24172  subgnm  24660  subgngp  24662  lssnlm  24736  cmscsscms  25419  efgh  26592  efabl  26601  efsubm  26602  gsumsubg  33021  qusker  33334  eqgvscpbl  33335  grplsmid  33389  quslsm  33390  qusima  33393  nsgmgc  33397  nsgqusf1olem1  33398  nsgqusf1olem2  33399  nsgqusf1olem3  33400  qsnzr  33440  opprqusplusg  33474  opprqus0g  33475  algextdeglem1  33700  algextdeglem2  33701  algextdeglem3  33702  algextdeglem4  33703  algextdeglem5  33704  nelsubgcld  42385  nelsubgsubcld  42386  idomsubgmo  43094