Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elghomlem2OLD Structured version   Unicode version

Theorem elghomlem2OLD 26088
 Description: Obsolete as of 15-Mar-2020. Lemma for elghomOLD 26089. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypothesis
Ref Expression
elghomlem1OLD.1
Assertion
Ref Expression
elghomlem2OLD GrpOpHom
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem elghomlem2OLD
StepHypRef Expression
1 elghomlem1OLD.1 . . . 4
21elghomlem1OLD 26087 . . 3 GrpOpHom
32eleq2d 2492 . 2 GrpOpHom
4 elex 3089 . . . . 5
5 feq1 5728 . . . . . . . 8
6 fveq1 5880 . . . . . . . . . . 11
7 fveq1 5880 . . . . . . . . . . 11
86, 7oveq12d 6323 . . . . . . . . . 10
9 fveq1 5880 . . . . . . . . . 10
108, 9eqeq12d 2444 . . . . . . . . 9
11102ralbidv 2866 . . . . . . . 8
125, 11anbi12d 715 . . . . . . 7
1312, 1elab2g 3219 . . . . . 6
1413biimpd 210 . . . . 5
154, 14mpcom 37 . . . 4
16 rnexg 6739 . . . . . . 7
17 fex 6153 . . . . . . . 8
1817expcom 436 . . . . . . 7
1916, 18syl 17 . . . . . 6
2019adantrd 469 . . . . 5
2113biimprd 226 . . . . 5
2220, 21syli 38 . . . 4
2315, 22impbid2 207 . . 3