Theorem subggrp 17907

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 2797	. . . 4 ⊢ (Base‘𝐺) = (Base‘𝐺)
3	2	issubg 17904	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺 ↾s 𝑆) ∈ Grp))
4	3	simp3bi 1178	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp)
5	1, 4	syl5eqel 2880	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157   ⊆ wss 3767  ‘cfv 6099  (class class class)co 6876  Basecbs 16181   ↾_s cress 16182  Grpcgrp 17735  SubGrpcsubg 17898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ral 3092  df-rex 3093  df-rab 3096  df-v 3385  df-sbc 3632  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-br 4842  df-opab 4904  df-mpt 4921  df-id 5218  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-iota 6062  df-fun 6101  df-fv 6107  df-ov 6879  df-subg 17901

This theorem is referenced by:  subg0  17910  subginv  17911  subg0cl  17912  subginvcl  17913  subgcl  17914  issubg2  17919  issubgrpd  17921  subsubg  17927  resghm  17986  resghm2b  17988  subgga  18042  gasubg  18044  odsubdvds  18296  pgp0  18321  subgpgp  18322  sylow2blem2  18346  slwhash  18349  fislw  18350  subglsm  18396  pj1ghm  18426  subgabl  18553  cycsubgcyg  18614  subgdmdprd  18746  subgdprd  18747  ablfacrplem  18777  pgpfaclem1  18793  pgpfaclem3  18795  ablfaclem3  18799  issubrg2  19115  islss3  19277  mplgrp  19770  zringcyg  20158  cnmsgngrp  20243  psgnghm  20244  scmatghm  20662  m2cpmrngiso  20888  subgtgp  22234  subgngp  22764  reefgim  24542  amgmlemALT  43339