Metamath Proof Explorer

Theorem reuopreuprim

Description: There is a unique unordered pair with ordered elements fulfilling a wff if there is a unique ordered pair fulfilling the wff. (Contributed by AV, 28-Jul-2023)

Ref Expression
Assertion reuopreuprim 
|- ( X e. V -> ( E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ ph ) -> E! p e. ( Pairs ` X ) E. a E. b ( p = { a , b } /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( p = <. x , y >. -> ( p = <. a , b >. <-> <. x , y >. = <. a , b >. ) )
2 1 anbi1d 
 |-  ( p = <. x , y >. -> ( ( p = <. a , b >. /\ ph ) <-> ( <. x , y >. = <. a , b >. /\ ph ) ) )
3 2 2exbidv 
 |-  ( p = <. x , y >. -> ( E. a E. b ( p = <. a , b >. /\ ph ) <-> E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) ) )
4 eqeq1 
 |-  ( p = <. i , j >. -> ( p = <. a , b >. <-> <. i , j >. = <. a , b >. ) )
5 4 anbi1d 
 |-  ( p = <. i , j >. -> ( ( p = <. a , b >. /\ ph ) <-> ( <. i , j >. = <. a , b >. /\ ph ) ) )
6 5 2exbidv 
 |-  ( p = <. i , j >. -> ( E. a E. b ( p = <. a , b >. /\ ph ) <-> E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) ) )
7 3 6 reuop 
 |-  ( E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ ph ) <-> E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) )
8 simpll 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) -> x e. X )
9 simplr 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) -> y e. X )
10 oppr 
 |-  ( ( x e. _V /\ y e. _V ) -> ( <. x , y >. = <. a , b >. -> { x , y } = { a , b } ) )
11 10 el2v 
 |-  ( <. x , y >. = <. a , b >. -> { x , y } = { a , b } )
12 11 anim1i 
 |-  ( ( <. x , y >. = <. a , b >. /\ ph ) -> ( { x , y } = { a , b } /\ ph ) )
13 12 2eximi 
 |-  ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) -> E. a E. b ( { x , y } = { a , b } /\ ph ) )
14 13 adantr 
 |-  ( ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) -> E. a E. b ( { x , y } = { a , b } /\ ph ) )
15 14 adantl 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) -> E. a E. b ( { x , y } = { a , b } /\ ph ) )
16 nfv 
 |-  F/ a ( x e. X /\ y e. X )
17 nfe1 
 |-  F/ a E. a E. b ( <. x , y >. = <. a , b >. /\ ph )
18 nfcv 
 |-  F/_ a X
19 nfe1 
 |-  F/ a E. a E. b ( <. i , j >. = <. a , b >. /\ ph )
20 nfv 
 |-  F/ a <. i , j >. = <. x , y >.
21 19 20 nfim 
 |-  F/ a ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. )
22 18 21 nfralw 
 |-  F/ a A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. )
23 18 22 nfralw 
 |-  F/ a A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. )
24 17 23 nfan 
 |-  F/ a ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) )
25 16 24 nfan 
 |-  F/ a ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) )
26 nfv 
 |-  F/ a ( m e. X /\ n e. X )
27 25 26 nfan 
 |-  F/ a ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) )
28 nfv 
 |-  F/ a { m , n } = { x , y }
29 nfv 
 |-  F/ b ( x e. X /\ y e. X )
30 nfe1 
 |-  F/ b E. b ( <. x , y >. = <. a , b >. /\ ph )
31 30 nfex 
 |-  F/ b E. a E. b ( <. x , y >. = <. a , b >. /\ ph )
32 nfcv 
 |-  F/_ b X
33 nfe1 
 |-  F/ b E. b ( <. i , j >. = <. a , b >. /\ ph )
34 33 nfex 
 |-  F/ b E. a E. b ( <. i , j >. = <. a , b >. /\ ph )
35 nfv 
 |-  F/ b <. i , j >. = <. x , y >.
36 34 35 nfim 
 |-  F/ b ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. )
37 32 36 nfralw 
 |-  F/ b A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. )
38 32 37 nfralw 
 |-  F/ b A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. )
39 31 38 nfan 
 |-  F/ b ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) )
40 29 39 nfan 
 |-  F/ b ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) )
41 nfv 
 |-  F/ b ( m e. X /\ n e. X )
42 40 41 nfan 
 |-  F/ b ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) )
43 nfv 
 |-  F/ b { m , n } = { x , y }
44 vex 
 |-  m e. _V
45 vex 
 |-  n e. _V
46 vex 
 |-  a e. _V
47 vex 
 |-  b e. _V
48 44 45 46 47 preq12b 
 |-  ( { m , n } = { a , b } <-> ( ( m = a /\ n = b ) \/ ( m = b /\ n = a ) ) )
49 opeq1 
 |-  ( i = m -> <. i , j >. = <. m , j >. )
50 49 eqeq1d 
 |-  ( i = m -> ( <. i , j >. = <. a , b >. <-> <. m , j >. = <. a , b >. ) )
51 50 anbi1d 
 |-  ( i = m -> ( ( <. i , j >. = <. a , b >. /\ ph ) <-> ( <. m , j >. = <. a , b >. /\ ph ) ) )
52 51 2exbidv 
 |-  ( i = m -> ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) <-> E. a E. b ( <. m , j >. = <. a , b >. /\ ph ) ) )
53 49 eqeq1d 
 |-  ( i = m -> ( <. i , j >. = <. x , y >. <-> <. m , j >. = <. x , y >. ) )
54 52 53 imbi12d 
 |-  ( i = m -> ( ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) <-> ( E. a E. b ( <. m , j >. = <. a , b >. /\ ph ) -> <. m , j >. = <. x , y >. ) ) )
55 opeq2 
 |-  ( j = n -> <. m , j >. = <. m , n >. )
56 55 eqeq1d 
 |-  ( j = n -> ( <. m , j >. = <. a , b >. <-> <. m , n >. = <. a , b >. ) )
57 56 anbi1d 
 |-  ( j = n -> ( ( <. m , j >. = <. a , b >. /\ ph ) <-> ( <. m , n >. = <. a , b >. /\ ph ) ) )
58 57 2exbidv 
 |-  ( j = n -> ( E. a E. b ( <. m , j >. = <. a , b >. /\ ph ) <-> E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) ) )
59 55 eqeq1d 
 |-  ( j = n -> ( <. m , j >. = <. x , y >. <-> <. m , n >. = <. x , y >. ) )
60 58 59 imbi12d 
 |-  ( j = n -> ( ( E. a E. b ( <. m , j >. = <. a , b >. /\ ph ) -> <. m , j >. = <. x , y >. ) <-> ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) ) )
61 54 60 rspc2v 
 |-  ( ( m e. X /\ n e. X ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) ) )
62 pm3.22 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( x e. X /\ y e. X ) ) -> ( ( x e. X /\ y e. X ) /\ ( m e. X /\ n e. X ) ) )
63 62 3adant2 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) -> ( ( x e. X /\ y e. X ) /\ ( m e. X /\ n e. X ) ) )
64 63 adantr 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> ( ( x e. X /\ y e. X ) /\ ( m e. X /\ n e. X ) ) )
65 eqidd 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> <. m , n >. = <. m , n >. )
66 sbceq1a 
 |-  ( a = m -> ( ph <-> [. m / a ]. ph ) )
67 66 equcoms 
 |-  ( m = a -> ( ph <-> [. m / a ]. ph ) )
68 sbceq1a 
 |-  ( b = n -> ( [. m / a ]. ph <-> [. n / b ]. [. m / a ]. ph ) )
69 68 equcoms 
 |-  ( n = b -> ( [. m / a ]. ph <-> [. n / b ]. [. m / a ]. ph ) )
70 67 69 sylan9bb 
 |-  ( ( m = a /\ n = b ) -> ( ph <-> [. n / b ]. [. m / a ]. ph ) )
71 70 3ad2ant2 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) -> ( ph <-> [. n / b ]. [. m / a ]. ph ) )
72 71 biimpa 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> [. n / b ]. [. m / a ]. ph )
73 64 65 72 jca32 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> ( ( ( x e. X /\ y e. X ) /\ ( m e. X /\ n e. X ) ) /\ ( <. m , n >. = <. m , n >. /\ [. n / b ]. [. m / a ]. ph ) ) )
74 nfv 
 |-  F/ a <. m , n >. = <. m , n >.
75 nfcv 
 |-  F/_ a n
76 nfsbc1v 
 |-  F/ a [. m / a ]. ph
77 75 76 nfsbcw 
 |-  F/ a [. n / b ]. [. m / a ]. ph
78 74 77 nfan 
 |-  F/ a ( <. m , n >. = <. m , n >. /\ [. n / b ]. [. m / a ]. ph )
79 nfv 
 |-  F/ b <. m , n >. = <. m , n >.
80 nfsbc1v 
 |-  F/ b [. n / b ]. [. m / a ]. ph
81 79 80 nfan 
 |-  F/ b ( <. m , n >. = <. m , n >. /\ [. n / b ]. [. m / a ]. ph )
82 opeq12 
 |-  ( ( a = m /\ b = n ) -> <. a , b >. = <. m , n >. )
83 82 eqeq2d 
 |-  ( ( a = m /\ b = n ) -> ( <. m , n >. = <. a , b >. <-> <. m , n >. = <. m , n >. ) )
84 66 68 sylan9bb 
 |-  ( ( a = m /\ b = n ) -> ( ph <-> [. n / b ]. [. m / a ]. ph ) )
85 83 84 anbi12d 
 |-  ( ( a = m /\ b = n ) -> ( ( <. m , n >. = <. a , b >. /\ ph ) <-> ( <. m , n >. = <. m , n >. /\ [. n / b ]. [. m / a ]. ph ) ) )
86 85 adantl 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( a = m /\ b = n ) ) -> ( ( <. m , n >. = <. a , b >. /\ ph ) <-> ( <. m , n >. = <. m , n >. /\ [. n / b ]. [. m / a ]. ph ) ) )
87 78 81 86 spc2ed 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( m e. X /\ n e. X ) ) -> ( ( <. m , n >. = <. m , n >. /\ [. n / b ]. [. m / a ]. ph ) -> E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) ) )
88 87 imp 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( m e. X /\ n e. X ) ) /\ ( <. m , n >. = <. m , n >. /\ [. n / b ]. [. m / a ]. ph ) ) -> E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) )
89 pm2.27 
 |-  ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> ( ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) -> <. m , n >. = <. x , y >. ) )
90 73 88 89 3syl 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> ( ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) -> <. m , n >. = <. x , y >. ) )
91 oppr 
 |-  ( ( m e. _V /\ n e. _V ) -> ( <. m , n >. = <. x , y >. -> { m , n } = { x , y } ) )
92 91 el2v 
 |-  ( <. m , n >. = <. x , y >. -> { m , n } = { x , y } )
93 90 92 syl6 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> ( ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) -> { m , n } = { x , y } ) )
94 93 ex 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) -> ( ph -> ( ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) -> { m , n } = { x , y } ) ) )
95 94 com23 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( m = a /\ n = b ) /\ ( x e. X /\ y e. X ) ) -> ( ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) -> ( ph -> { m , n } = { x , y } ) ) )
96 95 3exp 
 |-  ( ( m e. X /\ n e. X ) -> ( ( m = a /\ n = b ) -> ( ( x e. X /\ y e. X ) -> ( ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) -> ( ph -> { m , n } = { x , y } ) ) ) ) )
97 96 com24 
 |-  ( ( m e. X /\ n e. X ) -> ( ( E. a E. b ( <. m , n >. = <. a , b >. /\ ph ) -> <. m , n >. = <. x , y >. ) -> ( ( x e. X /\ y e. X ) -> ( ( m = a /\ n = b ) -> ( ph -> { m , n } = { x , y } ) ) ) ) )
98 61 97 syld 
 |-  ( ( m e. X /\ n e. X ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( ( x e. X /\ y e. X ) -> ( ( m = a /\ n = b ) -> ( ph -> { m , n } = { x , y } ) ) ) ) )
99 98 com13 
 |-  ( ( x e. X /\ y e. X ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( ( m e. X /\ n e. X ) -> ( ( m = a /\ n = b ) -> ( ph -> { m , n } = { x , y } ) ) ) ) )
100 99 a1d 
 |-  ( ( x e. X /\ y e. X ) -> ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( ( m e. X /\ n e. X ) -> ( ( m = a /\ n = b ) -> ( ph -> { m , n } = { x , y } ) ) ) ) ) )
101 100 imp42 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) ) -> ( ( m = a /\ n = b ) -> ( ph -> { m , n } = { x , y } ) ) )
102 opeq1 
 |-  ( i = n -> <. i , j >. = <. n , j >. )
103 102 eqeq1d 
 |-  ( i = n -> ( <. i , j >. = <. a , b >. <-> <. n , j >. = <. a , b >. ) )
104 103 anbi1d 
 |-  ( i = n -> ( ( <. i , j >. = <. a , b >. /\ ph ) <-> ( <. n , j >. = <. a , b >. /\ ph ) ) )
105 104 2exbidv 
 |-  ( i = n -> ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) <-> E. a E. b ( <. n , j >. = <. a , b >. /\ ph ) ) )
106 102 eqeq1d 
 |-  ( i = n -> ( <. i , j >. = <. x , y >. <-> <. n , j >. = <. x , y >. ) )
107 105 106 imbi12d 
 |-  ( i = n -> ( ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) <-> ( E. a E. b ( <. n , j >. = <. a , b >. /\ ph ) -> <. n , j >. = <. x , y >. ) ) )
108 opeq2 
 |-  ( j = m -> <. n , j >. = <. n , m >. )
109 108 eqeq1d 
 |-  ( j = m -> ( <. n , j >. = <. a , b >. <-> <. n , m >. = <. a , b >. ) )
110 109 anbi1d 
 |-  ( j = m -> ( ( <. n , j >. = <. a , b >. /\ ph ) <-> ( <. n , m >. = <. a , b >. /\ ph ) ) )
111 110 2exbidv 
 |-  ( j = m -> ( E. a E. b ( <. n , j >. = <. a , b >. /\ ph ) <-> E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) ) )
112 108 eqeq1d 
 |-  ( j = m -> ( <. n , j >. = <. x , y >. <-> <. n , m >. = <. x , y >. ) )
113 111 112 imbi12d 
 |-  ( j = m -> ( ( E. a E. b ( <. n , j >. = <. a , b >. /\ ph ) -> <. n , j >. = <. x , y >. ) <-> ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) ) )
114 107 113 rspc2v 
 |-  ( ( n e. X /\ m e. X ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) ) )
115 114 ancoms 
 |-  ( ( m e. X /\ n e. X ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) ) )
116 pm3.22 
 |-  ( ( m e. X /\ n e. X ) -> ( n e. X /\ m e. X ) )
117 116 anim1ci 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( x e. X /\ y e. X ) ) -> ( ( x e. X /\ y e. X ) /\ ( n e. X /\ m e. X ) ) )
118 117 3adant2 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) -> ( ( x e. X /\ y e. X ) /\ ( n e. X /\ m e. X ) ) )
119 118 adantr 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> ( ( x e. X /\ y e. X ) /\ ( n e. X /\ m e. X ) ) )
120 eqidd 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> <. n , m >. = <. n , m >. )
121 sbceq1a 
 |-  ( b = m -> ( ph <-> [. m / b ]. ph ) )
122 121 equcoms 
 |-  ( m = b -> ( ph <-> [. m / b ]. ph ) )
123 sbceq1a 
 |-  ( a = n -> ( [. m / b ]. ph <-> [. n / a ]. [. m / b ]. ph ) )
124 123 equcoms 
 |-  ( n = a -> ( [. m / b ]. ph <-> [. n / a ]. [. m / b ]. ph ) )
125 122 124 sylan9bb 
 |-  ( ( m = b /\ n = a ) -> ( ph <-> [. n / a ]. [. m / b ]. ph ) )
126 125 3ad2ant2 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) -> ( ph <-> [. n / a ]. [. m / b ]. ph ) )
127 126 biimpa 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> [. n / a ]. [. m / b ]. ph )
128 119 120 127 jca32 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> ( ( ( x e. X /\ y e. X ) /\ ( n e. X /\ m e. X ) ) /\ ( <. n , m >. = <. n , m >. /\ [. n / a ]. [. m / b ]. ph ) ) )
129 nfv 
 |-  F/ a <. n , m >. = <. n , m >.
130 nfsbc1v 
 |-  F/ a [. n / a ]. [. m / b ]. ph
131 129 130 nfan 
 |-  F/ a ( <. n , m >. = <. n , m >. /\ [. n / a ]. [. m / b ]. ph )
132 nfv 
 |-  F/ b <. n , m >. = <. n , m >.
133 nfcv 
 |-  F/_ b n
134 nfsbc1v 
 |-  F/ b [. m / b ]. ph
135 133 134 nfsbcw 
 |-  F/ b [. n / a ]. [. m / b ]. ph
136 132 135 nfan 
 |-  F/ b ( <. n , m >. = <. n , m >. /\ [. n / a ]. [. m / b ]. ph )
137 opeq12 
 |-  ( ( a = n /\ b = m ) -> <. a , b >. = <. n , m >. )
138 137 eqeq2d 
 |-  ( ( a = n /\ b = m ) -> ( <. n , m >. = <. a , b >. <-> <. n , m >. = <. n , m >. ) )
139 121 123 sylan9bbr 
 |-  ( ( a = n /\ b = m ) -> ( ph <-> [. n / a ]. [. m / b ]. ph ) )
140 138 139 anbi12d 
 |-  ( ( a = n /\ b = m ) -> ( ( <. n , m >. = <. a , b >. /\ ph ) <-> ( <. n , m >. = <. n , m >. /\ [. n / a ]. [. m / b ]. ph ) ) )
141 140 adantl 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( a = n /\ b = m ) ) -> ( ( <. n , m >. = <. a , b >. /\ ph ) <-> ( <. n , m >. = <. n , m >. /\ [. n / a ]. [. m / b ]. ph ) ) )
142 131 136 141 spc2ed 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( n e. X /\ m e. X ) ) -> ( ( <. n , m >. = <. n , m >. /\ [. n / a ]. [. m / b ]. ph ) -> E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) ) )
143 142 imp 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( n e. X /\ m e. X ) ) /\ ( <. n , m >. = <. n , m >. /\ [. n / a ]. [. m / b ]. ph ) ) -> E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) )
144 pm2.27 
 |-  ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> ( ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) -> <. n , m >. = <. x , y >. ) )
145 128 143 144 3syl 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> ( ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) -> <. n , m >. = <. x , y >. ) )
146 prcom 
 |-  { n , m } = { m , n }
147 oppr 
 |-  ( ( n e. _V /\ m e. _V ) -> ( <. n , m >. = <. x , y >. -> { n , m } = { x , y } ) )
148 147 el2v 
 |-  ( <. n , m >. = <. x , y >. -> { n , m } = { x , y } )
149 146 148 eqtr3id 
 |-  ( <. n , m >. = <. x , y >. -> { m , n } = { x , y } )
150 145 149 syl6 
 |-  ( ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) /\ ph ) -> ( ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) -> { m , n } = { x , y } ) )
151 150 ex 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) -> ( ph -> ( ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) -> { m , n } = { x , y } ) ) )
152 151 com23 
 |-  ( ( ( m e. X /\ n e. X ) /\ ( m = b /\ n = a ) /\ ( x e. X /\ y e. X ) ) -> ( ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) -> ( ph -> { m , n } = { x , y } ) ) )
153 152 3exp 
 |-  ( ( m e. X /\ n e. X ) -> ( ( m = b /\ n = a ) -> ( ( x e. X /\ y e. X ) -> ( ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) -> ( ph -> { m , n } = { x , y } ) ) ) ) )
154 153 com24 
 |-  ( ( m e. X /\ n e. X ) -> ( ( E. a E. b ( <. n , m >. = <. a , b >. /\ ph ) -> <. n , m >. = <. x , y >. ) -> ( ( x e. X /\ y e. X ) -> ( ( m = b /\ n = a ) -> ( ph -> { m , n } = { x , y } ) ) ) ) )
155 115 154 syld 
 |-  ( ( m e. X /\ n e. X ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( ( x e. X /\ y e. X ) -> ( ( m = b /\ n = a ) -> ( ph -> { m , n } = { x , y } ) ) ) ) )
156 155 com13 
 |-  ( ( x e. X /\ y e. X ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( ( m e. X /\ n e. X ) -> ( ( m = b /\ n = a ) -> ( ph -> { m , n } = { x , y } ) ) ) ) )
157 156 a1d 
 |-  ( ( x e. X /\ y e. X ) -> ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) -> ( A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) -> ( ( m e. X /\ n e. X ) -> ( ( m = b /\ n = a ) -> ( ph -> { m , n } = { x , y } ) ) ) ) ) )
158 157 imp42 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) ) -> ( ( m = b /\ n = a ) -> ( ph -> { m , n } = { x , y } ) ) )
159 101 158 jaod 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) ) -> ( ( ( m = a /\ n = b ) \/ ( m = b /\ n = a ) ) -> ( ph -> { m , n } = { x , y } ) ) )
160 48 159 syl5bi 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) ) -> ( { m , n } = { a , b } -> ( ph -> { m , n } = { x , y } ) ) )
161 160 impd 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) ) -> ( ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , y } ) )
162 42 43 161 exlimd 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) ) -> ( E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , y } ) )
163 27 28 162 exlimd 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) /\ ( m e. X /\ n e. X ) ) -> ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , y } ) )
164 163 ralrimivva 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) -> A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , y } ) )
165 preq1 
 |-  ( v = x -> { v , w } = { x , w } )
166 165 eqeq1d 
 |-  ( v = x -> ( { v , w } = { a , b } <-> { x , w } = { a , b } ) )
167 166 anbi1d 
 |-  ( v = x -> ( ( { v , w } = { a , b } /\ ph ) <-> ( { x , w } = { a , b } /\ ph ) ) )
168 167 2exbidv 
 |-  ( v = x -> ( E. a E. b ( { v , w } = { a , b } /\ ph ) <-> E. a E. b ( { x , w } = { a , b } /\ ph ) ) )
169 165 eqeq2d 
 |-  ( v = x -> ( { m , n } = { v , w } <-> { m , n } = { x , w } ) )
170 169 imbi2d 
 |-  ( v = x -> ( ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { v , w } ) <-> ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , w } ) ) )
171 170 2ralbidv 
 |-  ( v = x -> ( A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { v , w } ) <-> A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , w } ) ) )
172 168 171 anbi12d 
 |-  ( v = x -> ( ( E. a E. b ( { v , w } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { v , w } ) ) <-> ( E. a E. b ( { x , w } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , w } ) ) ) )
173 preq2 
 |-  ( w = y -> { x , w } = { x , y } )
174 173 eqeq1d 
 |-  ( w = y -> ( { x , w } = { a , b } <-> { x , y } = { a , b } ) )
175 174 anbi1d 
 |-  ( w = y -> ( ( { x , w } = { a , b } /\ ph ) <-> ( { x , y } = { a , b } /\ ph ) ) )
176 175 2exbidv 
 |-  ( w = y -> ( E. a E. b ( { x , w } = { a , b } /\ ph ) <-> E. a E. b ( { x , y } = { a , b } /\ ph ) ) )
177 173 eqeq2d 
 |-  ( w = y -> ( { m , n } = { x , w } <-> { m , n } = { x , y } ) )
178 177 imbi2d 
 |-  ( w = y -> ( ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , w } ) <-> ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , y } ) ) )
179 178 2ralbidv 
 |-  ( w = y -> ( A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , w } ) <-> A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , y } ) ) )
180 176 179 anbi12d 
 |-  ( w = y -> ( ( E. a E. b ( { x , w } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , w } ) ) <-> ( E. a E. b ( { x , y } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , y } ) ) ) )
181 172 180 rspc2ev 
 |-  ( ( x e. X /\ y e. X /\ ( E. a E. b ( { x , y } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { x , y } ) ) ) -> E. v e. X E. w e. X ( E. a E. b ( { v , w } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { v , w } ) ) )
182 8 9 15 164 181 syl112anc 
 |-  ( ( ( x e. X /\ y e. X ) /\ ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) ) -> E. v e. X E. w e. X ( E. a E. b ( { v , w } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { v , w } ) ) )
183 182 ex 
 |-  ( ( x e. X /\ y e. X ) -> ( ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) -> E. v e. X E. w e. X ( E. a E. b ( { v , w } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { v , w } ) ) ) )
184 183 rexlimivv 
 |-  ( E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) -> E. v e. X E. w e. X ( E. a E. b ( { v , w } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { v , w } ) ) )
185 eqeq1 
 |-  ( p = { v , w } -> ( p = { a , b } <-> { v , w } = { a , b } ) )
186 185 anbi1d 
 |-  ( p = { v , w } -> ( ( p = { a , b } /\ ph ) <-> ( { v , w } = { a , b } /\ ph ) ) )
187 186 2exbidv 
 |-  ( p = { v , w } -> ( E. a E. b ( p = { a , b } /\ ph ) <-> E. a E. b ( { v , w } = { a , b } /\ ph ) ) )
188 eqeq1 
 |-  ( p = { m , n } -> ( p = { a , b } <-> { m , n } = { a , b } ) )
189 188 anbi1d 
 |-  ( p = { m , n } -> ( ( p = { a , b } /\ ph ) <-> ( { m , n } = { a , b } /\ ph ) ) )
190 189 2exbidv 
 |-  ( p = { m , n } -> ( E. a E. b ( p = { a , b } /\ ph ) <-> E. a E. b ( { m , n } = { a , b } /\ ph ) ) )
191 187 190 reupr 
 |-  ( X e. V -> ( E! p e. ( Pairs ` X ) E. a E. b ( p = { a , b } /\ ph ) <-> E. v e. X E. w e. X ( E. a E. b ( { v , w } = { a , b } /\ ph ) /\ A. m e. X A. n e. X ( E. a E. b ( { m , n } = { a , b } /\ ph ) -> { m , n } = { v , w } ) ) ) )
192 184 191 syl5ibr 
 |-  ( X e. V -> ( E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. i e. X A. j e. X ( E. a E. b ( <. i , j >. = <. a , b >. /\ ph ) -> <. i , j >. = <. x , y >. ) ) -> E! p e. ( Pairs ` X ) E. a E. b ( p = { a , b } /\ ph ) ) )
193 7 192 syl5bi 
 |-  ( X e. V -> ( E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ ph ) -> E! p e. ( Pairs ` X ) E. a E. b ( p = { a , b } /\ ph ) ) )