Theorem subggrp 19198

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 2770	. . . 4 ⊢ (Base‘𝐺) = (Base‘𝐺)
3	2	issubg 19195	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺 ↾s 𝑆) ∈ Grp))
4	3	simp3bi 1163	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp)
5	1, 4	eqeltrid 2874	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2150   ⊆ wss 3913  ‘cfv 6540  (class class class)co 7414  Basecbs 17272   ↾_s cress 17293  Grpcgrp 19003  SubGrpcsubg 19189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-11 2199  ax-12 2220  ax-ext 2742  ax-sep 5262  ax-nul 5274  ax-pow 5340  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-nfc 2919  df-ne 2966  df-ral 3087  df-rex 3097  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5560  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7417  df-subg 19192

This theorem is referenced by:  subg0  19201  subginv  19202  subg0cl  19203  subginvcl  19204  subgcl  19205  issubg2  19211  issubgrpd  19213  subsubg  19219  resghm  19305  resghm2b  19307  subgga  19373  gasubg  19375  odsubdvds  19644  pgp0  19669  subgpgp  19670  sylow2blem2  19694  slwhash  19697  fislw  19698  subglsm  19746  pj1ghm  19776  subgabl  19909  cntrabl  19916  cycsubgcyg  19974  subgdmdprd  20109  subgdprd  20110  ablfacrplem  20140  pgpfaclem1  20156  pgpfaclem3  20158  ablfaclem3  20162  issubrg2  20680  subdrgint  20889  islss3  21063  zringcyg  21602  cnmsgngrp  21712  psgnghm  21713  mplgrp  22149  scmatghm  22673  subgtgp  24245  subgngp  24775  reefgim  26593  subgmulgcld  33333  ressply1sub  33830  amgmlemALT  50552