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 syl5bi
 |-  ( ( [ 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 syl5bir
 |-  ( ( [ 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 ) )