Theorem subgrcl 18760

Description: Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

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

Proof of Theorem subgrcl

Step	Hyp	Ref	Expression
1		eqid 2738	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2	1	issubg 18755	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺 ↾s 𝑆) ∈ Grp))
3	2	simp1bi 1144	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3887  ‘cfv 6433  (class class class)co 7275  Basecbs 16912   ↾_s cress 16941  Grpcgrp 18577  SubGrpcsubg 18749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-subg 18752

This theorem is referenced by:  subg0  18761  subginv  18762  subgmulgcl  18768  subgsubm  18777  subsubg  18778  subgint  18779  isnsg  18783  nsgconj  18787  isnsg3  18788  ssnmz  18794  nmznsg  18796  eqger  18806  eqgid  18808  eqgen  18809  eqgcpbl  18810  qusgrp  18811  quseccl  18812  qusadd  18813  qus0  18814  qusinv  18815  qussub  18816  resghm2  18851  resghm2b  18852  conjsubg  18866  conjsubgen  18867  conjnmz  18868  conjnmzb  18869  qusghm  18871  subgga  18906  gastacos  18916  orbstafun  18917  cntrsubgnsg  18947  oppgsubg  18970  isslw  19213  sylow2blem1  19225  sylow2blem2  19226  sylow2blem3  19227  slwhash  19229  lsmval  19253  lsmelval  19254  lsmelvali  19255  lsmelvalm  19256  lsmsubg  19259  lsmless1  19265  lsmless2  19266  lsmless12  19267  lsmass  19275  lsm01  19277  lsm02  19278  subglsm  19279  lsmmod  19281  lsmcntz  19285  lsmcntzr  19286  lsmdisj2  19288  subgdisj1  19297  pj1f  19303  pj1id  19305  pj1lid  19307  pj1rid  19308  pj1ghm  19309  subgdmdprd  19637  subgdprd  19638  dprdsn  19639  pgpfaclem2  19685  cldsubg  23262  gsumsubg  31306  qusker  31549  grplsmid  31592  quslsm  31593  nsgqus0  31595  nsgmgclem  31596  nsgqusf1olem1  31598  nsgqusf1olem2  31599  nsgqusf1olem3  31600