Theorem subggrp 18274

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

Syntax hints:   → wi 4   = wceq 1531   ∈ wcel 2108   ⊆ wss 3934  ‘cfv 6348  (class class class)co 7148  Basecbs 16475   ↾_s cress 16476  Grpcgrp 18095  SubGrpcsubg 18265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7151  df-subg 18268

This theorem is referenced by:  subg0  18277  subginv  18278  subg0cl  18279  subginvcl  18280  subgcl  18281  issubg2  18286  issubgrpd  18288  subsubg  18294  resghm  18366  resghm2b  18368  subgga  18422  gasubg  18424  odsubdvds  18688  pgp0  18713  subgpgp  18714  sylow2blem2  18738  slwhash  18741  fislw  18742  subglsm  18791  pj1ghm  18821  subgabl  18948  cntrabl  18955  cycsubgcyg  19013  subgdmdprd  19148  subgdprd  19149  ablfacrplem  19179  pgpfaclem1  19195  pgpfaclem3  19197  ablfaclem3  19201  issubrg2  19547  subdrgint  19574  islss3  19723  mplgrp  20222  zringcyg  20630  cnmsgngrp  20715  psgnghm  20716  scmatghm  21134  m2cpmrngiso  21358  subgtgp  22705  subgngp  23236  reefgim  25030  amgmlemALT  44895