Theorem subggrp 19046

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ⊆ wss 3940  ‘cfv 6533  (class class class)co 7401  Basecbs 17143   ↾_s cress 17172  Grpcgrp 18853  SubGrpcsubg 19037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fv 6541  df-ov 7404  df-subg 19040

This theorem is referenced by:  subg0  19049  subginv  19050  subg0cl  19051  subginvcl  19052  subgcl  19053  issubg2  19058  issubgrpd  19060  subsubg  19066  resghm  19147  resghm2b  19149  subgga  19206  gasubg  19208  odsubdvds  19481  pgp0  19506  subgpgp  19507  sylow2blem2  19531  slwhash  19534  fislw  19535  subglsm  19583  pj1ghm  19613  subgabl  19746  cntrabl  19753  cycsubgcyg  19811  subgdmdprd  19946  subgdprd  19947  ablfacrplem  19977  pgpfaclem1  19993  pgpfaclem3  19995  ablfaclem3  19999  issubrg2  20484  subdrgint  20644  islss3  20796  zringcyg  21324  cnmsgngrp  21440  psgnghm  21441  mplgrp  21886  scmatghm  22357  subgtgp  23931  subgngp  24466  reefgim  26304  ressply1sub  33126  amgmlemALT  48038