Metamath Proof Explorer


Theorem grpinv11OLD

Description: Obsolete version of grpinv11 as of 8-Jul-2025. (Contributed by NM, 22-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses grpinvinv.b B = Base G
grpinvinv.n N = inv g G
grpinv11.g φ G Grp
grpinv11.x φ X B
grpinv11.y φ Y B
Assertion grpinv11OLD φ N X = N Y X = Y

Proof

Step Hyp Ref Expression
1 grpinvinv.b B = Base G
2 grpinvinv.n N = inv g G
3 grpinv11.g φ G Grp
4 grpinv11.x φ X B
5 grpinv11.y φ Y B
6 fveq2 N X = N Y N N X = N N Y
7 6 adantl φ N X = N Y N N X = N N Y
8 1 2 grpinvinv G Grp X B N N X = X
9 3 4 8 syl2anc φ N N X = X
10 9 adantr φ N X = N Y N N X = X
11 1 2 grpinvinv G Grp Y B N N Y = Y
12 3 5 11 syl2anc φ N N Y = Y
13 12 adantr φ N X = N Y N N Y = Y
14 7 10 13 3eqtr3d φ N X = N Y X = Y
15 14 ex φ N X = N Y X = Y
16 fveq2 X = Y N X = N Y
17 15 16 impbid1 φ N X = N Y X = Y