Metamath Proof Explorer

Theorem ichnreuop

Description: If the setvar variables are interchangeable in a wff, there is never a unique ordered pair with different components fulfilling the wff (because if <. a , b >. fulfils the wff, then also <. b , a >. fulfils the wff). (Contributed by AV, 27-Aug-2023)

Ref Expression
Assertion ichnreuop 
|- ( [ a <> b ] ph -> -. E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) )

Proof

Step Hyp Ref Expression
1 notnotb 
 |-  ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) <-> -. -. E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) )
2 nfv 
 |-  F/ c ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph )
3 nfv 
 |-  F/ d ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph )
4 nfv 
 |-  F/ a <. x , y >. = <. c , d >.
5 nfv 
 |-  F/ a c =/= d
6 nfsbc1v 
 |-  F/ a [. c / a ]. [. d / b ]. ph
7 4 5 6 nf3an 
 |-  F/ a ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph )
8 nfv 
 |-  F/ b <. x , y >. = <. c , d >.
9 nfv 
 |-  F/ b c =/= d
10 nfcv 
 |-  F/_ b c
11 nfsbc1v 
 |-  F/ b [. d / b ]. ph
12 10 11 nfsbcw 
 |-  F/ b [. c / a ]. [. d / b ]. ph
13 8 9 12 nf3an 
 |-  F/ b ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph )
14 opeq12 
 |-  ( ( a = c /\ b = d ) -> <. a , b >. = <. c , d >. )
15 14 eqeq2d 
 |-  ( ( a = c /\ b = d ) -> ( <. x , y >. = <. a , b >. <-> <. x , y >. = <. c , d >. ) )
16 simpl 
 |-  ( ( a = c /\ b = d ) -> a = c )
17 simpr 
 |-  ( ( a = c /\ b = d ) -> b = d )
18 16 17 neeq12d 
 |-  ( ( a = c /\ b = d ) -> ( a =/= b <-> c =/= d ) )
19 sbceq1a 
 |-  ( b = d -> ( ph <-> [. d / b ]. ph ) )
20 sbceq1a 
 |-  ( a = c -> ( [. d / b ]. ph <-> [. c / a ]. [. d / b ]. ph ) )
21 19 20 sylan9bbr 
 |-  ( ( a = c /\ b = d ) -> ( ph <-> [. c / a ]. [. d / b ]. ph ) )
22 15 18 21 3anbi123d 
 |-  ( ( a = c /\ b = d ) -> ( ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) )
23 2 3 7 13 22 cbvex2v 
 |-  ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) <-> E. c E. d ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) )
24 vex 
 |-  x e. _V
25 vex 
 |-  y e. _V
26 24 25 opth 
 |-  ( <. x , y >. = <. c , d >. <-> ( x = c /\ y = d ) )
27 eleq1w 
 |-  ( y = d -> ( y e. X <-> d e. X ) )
28 27 biimpcd 
 |-  ( y e. X -> ( y = d -> d e. X ) )
29 28 adantl 
 |-  ( ( x e. X /\ y e. X ) -> ( y = d -> d e. X ) )
30 29 adantl 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( y = d -> d e. X ) )
31 30 com12 
 |-  ( y = d -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> d e. X ) )
32 31 adantl 
 |-  ( ( x = c /\ y = d ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> d e. X ) )
33 26 32 sylbi 
 |-  ( <. x , y >. = <. c , d >. -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> d e. X ) )
34 33 3ad2ant1 
 |-  ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> d e. X ) )
35 34 impcom 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> d e. X )
36 eleq1w 
 |-  ( x = c -> ( x e. X <-> c e. X ) )
37 36 biimpcd 
 |-  ( x e. X -> ( x = c -> c e. X ) )
38 37 adantr 
 |-  ( ( x e. X /\ y e. X ) -> ( x = c -> c e. X ) )
39 38 adantl 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( x = c -> c e. X ) )
40 39 com12 
 |-  ( x = c -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> c e. X ) )
41 40 adantr 
 |-  ( ( x = c /\ y = d ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> c e. X ) )
42 26 41 sylbi 
 |-  ( <. x , y >. = <. c , d >. -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> c e. X ) )
43 42 3ad2ant1 
 |-  ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> c e. X ) )
44 43 impcom 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> c e. X )
45 eqidd 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> <. d , c >. = <. d , c >. )
46 necom 
 |-  ( c =/= d <-> d =/= c )
47 46 biimpi 
 |-  ( c =/= d -> d =/= c )
48 47 3ad2ant2 
 |-  ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> d =/= c )
49 48 adantl 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> d =/= c )
50 dfich2 
 |-  ( [ a <> b ] ph <-> A. c A. d ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) )
51 2sp 
 |-  ( A. c A. d ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) -> ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) )
52 sbsbc 
 |-  ( [ d / b ] ph <-> [. d / b ]. ph )
53 52 sbbii 
 |-  ( [ c / a ] [ d / b ] ph <-> [ c / a ] [. d / b ]. ph )
54 sbsbc 
 |-  ( [ c / a ] [. d / b ]. ph <-> [. c / a ]. [. d / b ]. ph )
55 53 54 bitri 
 |-  ( [ c / a ] [ d / b ] ph <-> [. c / a ]. [. d / b ]. ph )
56 sbsbc 
 |-  ( [ c / b ] ph <-> [. c / b ]. ph )
57 56 sbbii 
 |-  ( [ d / a ] [ c / b ] ph <-> [ d / a ] [. c / b ]. ph )
58 sbsbc 
 |-  ( [ d / a ] [. c / b ]. ph <-> [. d / a ]. [. c / b ]. ph )
59 57 58 bitri 
 |-  ( [ d / a ] [ c / b ] ph <-> [. d / a ]. [. c / b ]. ph )
60 51 55 59 3bitr3g 
 |-  ( A. c A. d ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) -> ( [. c / a ]. [. d / b ]. ph <-> [. d / a ]. [. c / b ]. ph ) )
61 60 biimpd 
 |-  ( A. c A. d ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) -> ( [. c / a ]. [. d / b ]. ph -> [. d / a ]. [. c / b ]. ph ) )
62 50 61 sylbi 
 |-  ( [ a <> b ] ph -> ( [. c / a ]. [. d / b ]. ph -> [. d / a ]. [. c / b ]. ph ) )
63 62 adantr 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( [. c / a ]. [. d / b ]. ph -> [. d / a ]. [. c / b ]. ph ) )
64 63 com12 
 |-  ( [. c / a ]. [. d / b ]. ph -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> [. d / a ]. [. c / b ]. ph ) )
65 64 3ad2ant3 
 |-  ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> [. d / a ]. [. c / b ]. ph ) )
66 65 impcom 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> [. d / a ]. [. c / b ]. ph )
67 sbccom 
 |-  ( [. c / b ]. [. d / a ]. ph <-> [. d / a ]. [. c / b ]. ph )
68 66 67 sylibr 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> [. c / b ]. [. d / a ]. ph )
69 45 49 68 3jca 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> ( <. d , c >. = <. d , c >. /\ d =/= c /\ [. c / b ]. [. d / a ]. ph ) )
70 nfv 
 |-  F/ b <. d , c >. = <. d , c >.
71 nfv 
 |-  F/ b d =/= c
72 nfsbc1v 
 |-  F/ b [. c / b ]. [. d / a ]. ph
73 70 71 72 nf3an 
 |-  F/ b ( <. d , c >. = <. d , c >. /\ d =/= c /\ [. c / b ]. [. d / a ]. ph )
74 opeq2 
 |-  ( b = c -> <. d , b >. = <. d , c >. )
75 74 eqeq2d 
 |-  ( b = c -> ( <. d , c >. = <. d , b >. <-> <. d , c >. = <. d , c >. ) )
76 neeq2 
 |-  ( b = c -> ( d =/= b <-> d =/= c ) )
77 sbceq1a 
 |-  ( b = c -> ( [. d / a ]. ph <-> [. c / b ]. [. d / a ]. ph ) )
78 75 76 77 3anbi123d 
 |-  ( b = c -> ( ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) <-> ( <. d , c >. = <. d , c >. /\ d =/= c /\ [. c / b ]. [. d / a ]. ph ) ) )
79 10 73 78 spcegf 
 |-  ( c e. X -> ( ( <. d , c >. = <. d , c >. /\ d =/= c /\ [. c / b ]. [. d / a ]. ph ) -> E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) ) )
80 44 69 79 sylc 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) )
81 nfcv 
 |-  F/_ a d
82 nfv 
 |-  F/ a <. d , c >. = <. d , b >.
83 nfv 
 |-  F/ a d =/= b
84 nfsbc1v 
 |-  F/ a [. d / a ]. ph
85 82 83 84 nf3an 
 |-  F/ a ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph )
86 85 nfex 
 |-  F/ a E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph )
87 opeq1 
 |-  ( a = d -> <. a , b >. = <. d , b >. )
88 87 eqeq2d 
 |-  ( a = d -> ( <. d , c >. = <. a , b >. <-> <. d , c >. = <. d , b >. ) )
89 neeq1 
 |-  ( a = d -> ( a =/= b <-> d =/= b ) )
90 sbceq1a 
 |-  ( a = d -> ( ph <-> [. d / a ]. ph ) )
91 88 89 90 3anbi123d 
 |-  ( a = d -> ( ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) ) )
92 91 exbidv 
 |-  ( a = d -> ( E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) <-> E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) ) )
93 81 86 92 spcegf 
 |-  ( d e. X -> ( E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) -> E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) ) )
94 35 80 93 sylc 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) )
95 vex 
 |-  d e. _V
96 vex 
 |-  c e. _V
97 95 96 opth1 
 |-  ( <. d , c >. = <. c , d >. -> d = c )
98 97 equcomd 
 |-  ( <. d , c >. = <. c , d >. -> c = d )
99 98 necon3ai 
 |-  ( c =/= d -> -. <. d , c >. = <. c , d >. )
100 99 adantl 
 |-  ( ( <. x , y >. = <. c , d >. /\ c =/= d ) -> -. <. d , c >. = <. c , d >. )
101 eqeq2 
 |-  ( <. x , y >. = <. c , d >. -> ( <. d , c >. = <. x , y >. <-> <. d , c >. = <. c , d >. ) )
102 101 adantr 
 |-  ( ( <. x , y >. = <. c , d >. /\ c =/= d ) -> ( <. d , c >. = <. x , y >. <-> <. d , c >. = <. c , d >. ) )
103 100 102 mtbird 
 |-  ( ( <. x , y >. = <. c , d >. /\ c =/= d ) -> -. <. d , c >. = <. x , y >. )
104 103 3adant3 
 |-  ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> -. <. d , c >. = <. x , y >. )
105 104 adantl 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> -. <. d , c >. = <. x , y >. )
106 94 105 jcnd 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> -. ( E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , c >. = <. x , y >. ) )
107 opeq1 
 |-  ( v = d -> <. v , w >. = <. d , w >. )
108 107 eqeq1d 
 |-  ( v = d -> ( <. v , w >. = <. a , b >. <-> <. d , w >. = <. a , b >. ) )
109 108 3anbi1d 
 |-  ( v = d -> ( ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) ) )
110 109 2exbidv 
 |-  ( v = d -> ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) <-> E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) ) )
111 107 eqeq1d 
 |-  ( v = d -> ( <. v , w >. = <. x , y >. <-> <. d , w >. = <. x , y >. ) )
112 110 111 imbi12d 
 |-  ( v = d -> ( ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) <-> ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , w >. = <. x , y >. ) ) )
113 112 notbid 
 |-  ( v = d -> ( -. ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) <-> -. ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , w >. = <. x , y >. ) ) )
114 opeq2 
 |-  ( w = c -> <. d , w >. = <. d , c >. )
115 114 eqeq1d 
 |-  ( w = c -> ( <. d , w >. = <. a , b >. <-> <. d , c >. = <. a , b >. ) )
116 115 3anbi1d 
 |-  ( w = c -> ( ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) ) )
117 116 2exbidv 
 |-  ( w = c -> ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) <-> E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) ) )
118 114 eqeq1d 
 |-  ( w = c -> ( <. d , w >. = <. x , y >. <-> <. d , c >. = <. x , y >. ) )
119 117 118 imbi12d 
 |-  ( w = c -> ( ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , w >. = <. x , y >. ) <-> ( E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , c >. = <. x , y >. ) ) )
120 119 notbid 
 |-  ( w = c -> ( -. ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , w >. = <. x , y >. ) <-> -. ( E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , c >. = <. x , y >. ) ) )
121 113 120 rspc2ev 
 |-  ( ( d e. X /\ c e. X /\ -. ( E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , c >. = <. x , y >. ) ) -> E. v e. X E. w e. X -. ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) )
122 35 44 106 121 syl3anc 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> E. v e. X E. w e. X -. ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) )
123 rexnal2 
 |-  ( E. v e. X E. w e. X -. ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) <-> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) )
124 122 123 sylib 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) )
125 124 ex 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
126 125 exlimdvv 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( E. c E. d ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
127 23 126 biimtrid 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
128 1 127 biimtrrid 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( -. -. E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
129 128 orrd 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( -. E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) \/ -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
130 ianor 
 |-  ( -. ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) <-> ( -. E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) \/ -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
131 129 130 sylibr 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> -. ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
132 131 ralrimivva 
 |-  ( [ a <> b ] ph -> A. x e. X A. y e. X -. ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
133 ralnex2 
 |-  ( A. x e. X A. y e. X -. ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) <-> -. E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
134 132 133 sylib 
 |-  ( [ a <> b ] ph -> -. E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
135 eqeq1 
 |-  ( p = <. x , y >. -> ( p = <. a , b >. <-> <. x , y >. = <. a , b >. ) )
136 135 3anbi1d 
 |-  ( p = <. x , y >. -> ( ( p = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) ) )
137 136 2exbidv 
 |-  ( p = <. x , y >. -> ( E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) <-> E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) ) )
138 eqeq1 
 |-  ( p = <. v , w >. -> ( p = <. a , b >. <-> <. v , w >. = <. a , b >. ) )
139 138 3anbi1d 
 |-  ( p = <. v , w >. -> ( ( p = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) ) )
140 139 2exbidv 
 |-  ( p = <. v , w >. -> ( E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) <-> E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) ) )
141 137 140 reuop 
 |-  ( E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) <-> E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
142 134 141 sylnibr 
 |-  ( [ a <> b ] ph -> -. E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) )