Metamath Proof Explorer


Theorem copsexg

Description: Substitution of class A for ordered pair <. x , y >. . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker copsexgw when possible. (Contributed by NM, 27-Dec-1996) (Revised by Andrew Salmon, 11-Jul-2011) (Proof shortened by Wolf Lammen, 25-Aug-2019) (New usage is discouraged.)

Ref Expression
Assertion copsexg A = x y φ x y A = x y φ

Proof

Step Hyp Ref Expression
1 vex x V
2 vex y V
3 1 2 eqvinop A = x y z w A = z w z w = x y
4 19.8a y z w = x y φ x y z w = x y φ
5 4 19.23bi z w = x y φ x y z w = x y φ
6 5 ex z w = x y φ x y z w = x y φ
7 vex z V
8 vex w V
9 7 8 opth z w = x y z = x w = y
10 9 anbi1i z w = x y φ z = x w = y φ
11 10 2exbii x y z w = x y φ x y z = x w = y φ
12 nfe1 x x z = x y w = y φ
13 19.8a w = y φ y w = y φ
14 13 anim2i z = x w = y φ z = x y w = y φ
15 14 anassrs z = x w = y φ z = x y w = y φ
16 15 eximi y z = x w = y φ y z = x y w = y φ
17 biidd y y = x z = x y w = y φ z = x y w = y φ
18 17 drex1 y y = x y z = x y w = y φ x z = x y w = y φ
19 16 18 syl5ib y y = x y z = x w = y φ x z = x y w = y φ
20 anass z = x w = y φ z = x w = y φ
21 20 exbii y z = x w = y φ y z = x w = y φ
22 19.40 y z = x w = y φ y z = x y w = y φ
23 nfeqf2 ¬ y y = x y z = x
24 23 19.9d ¬ y y = x y z = x z = x
25 24 anim1d ¬ y y = x y z = x y w = y φ z = x y w = y φ
26 22 25 syl5 ¬ y y = x y z = x w = y φ z = x y w = y φ
27 21 26 syl5bi ¬ y y = x y z = x w = y φ z = x y w = y φ
28 19.8a z = x y w = y φ x z = x y w = y φ
29 27 28 syl6 ¬ y y = x y z = x w = y φ x z = x y w = y φ
30 19 29 pm2.61i y z = x w = y φ x z = x y w = y φ
31 12 30 exlimi x y z = x w = y φ x z = x y w = y φ
32 euequ ∃! x x = z
33 equcom x = z z = x
34 33 eubii ∃! x x = z ∃! x z = x
35 32 34 mpbi ∃! x z = x
36 eupick ∃! x z = x x z = x y w = y φ z = x y w = y φ
37 35 36 mpan x z = x y w = y φ z = x y w = y φ
38 37 com12 z = x x z = x y w = y φ y w = y φ
39 euequ ∃! y y = w
40 equcom y = w w = y
41 40 eubii ∃! y y = w ∃! y w = y
42 39 41 mpbi ∃! y w = y
43 eupick ∃! y w = y y w = y φ w = y φ
44 42 43 mpan y w = y φ w = y φ
45 44 com12 w = y y w = y φ φ
46 38 45 sylan9 z = x w = y x z = x y w = y φ φ
47 31 46 syl5 z = x w = y x y z = x w = y φ φ
48 11 47 syl5bi z = x w = y x y z w = x y φ φ
49 9 48 sylbi z w = x y x y z w = x y φ φ
50 6 49 impbid z w = x y φ x y z w = x y φ
51 eqeq1 A = z w A = x y z w = x y
52 51 anbi1d A = z w A = x y φ z w = x y φ
53 52 2exbidv A = z w x y A = x y φ x y z w = x y φ
54 53 bibi2d A = z w φ x y A = x y φ φ x y z w = x y φ
55 51 54 imbi12d A = z w A = x y φ x y A = x y φ z w = x y φ x y z w = x y φ
56 50 55 mpbiri A = z w A = x y φ x y A = x y φ
57 56 adantr A = z w z w = x y A = x y φ x y A = x y φ
58 57 exlimivv z w A = z w z w = x y A = x y φ x y A = x y φ
59 3 58 sylbi A = x y A = x y φ x y A = x y φ
60 59 pm2.43i A = x y φ x y A = x y φ