Theorem subggrp 18349

Description: A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.)

Hypothesis

Ref	Expression
subggrp.h	⊢ 𝐻 = (𝐺 ↾s 𝑆)

Assertion

Ref	Expression
subggrp	⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)

Proof of Theorem subggrp

Step	Hyp	Ref	Expression
1		subggrp.h	. 2 ⊢ 𝐻 = (𝐺 ↾s 𝑆)
2		eqid 2758	. . . 4 ⊢ (Base‘𝐺) = (Base‘𝐺)
3	2	issubg 18346	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺 ↾s 𝑆) ∈ Grp))
4	3	simp3bi 1144	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp)
5	1, 4	eqeltrid 2856	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ⊆ wss 3858  ‘cfv 6335  (class class class)co 7150  Basecbs 16541   ↾_s cress 16542  Grpcgrp 18169  SubGrpcsubg 18340

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fv 6343  df-ov 7153  df-subg 18343

This theorem is referenced by:  subg0  18352  subginv  18353  subg0cl  18354  subginvcl  18355  subgcl  18356  issubg2  18361  issubgrpd  18363  subsubg  18369  resghm  18441  resghm2b  18443  subgga  18497  gasubg  18499  odsubdvds  18763  pgp0  18788  subgpgp  18789  sylow2blem2  18813  slwhash  18816  fislw  18817  subglsm  18866  pj1ghm  18896  subgabl  19024  cntrabl  19031  cycsubgcyg  19089  subgdmdprd  19224  subgdprd  19225  ablfacrplem  19255  pgpfaclem1  19271  pgpfaclem3  19273  ablfaclem3  19277  issubrg2  19623  subdrgint  19650  islss3  19799  zringcyg  20259  cnmsgngrp  20344  psgnghm  20345  mplgrp  20781  scmatghm  21233  m2cpmrngiso  21458  subgtgp  22805  subgngp  23337  reefgim  25144  amgmlemALT  45722