Metamath Proof Explorer

Theorem 2reu8i

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 . The involved wffs depend on the setvar variables as follows: ph(x,y), ta(v,y), ch(x,w), th(v,w), et(x,b), ps(a,b), ze(a,w). (Contributed by AV, 1-Apr-2023)

Ref Expression
Hypotheses 2reu8i.x 
|- ( x = v -> ( ph <-> ta ) )
2reu8i.v 
|- ( x = v -> ( ch <-> th ) )
2reu8i.w 
|- ( y = w -> ( ph <-> ch ) )
2reu8i.b 
|- ( y = b -> ( ph <-> et ) )
2reu8i.a 
|- ( x = a -> ( ch <-> ze ) )
2reu8i.1 
|- ( ( ( ch -> y = w ) /\ ze ) -> y = w )
2reu8i.2 
|- ( ( x = a /\ y = b ) -> ( ph <-> ps ) )
Assertion 2reu8i 
|- ( E! x e. A E! y e. B ph -> E. x e. A E. y e. B ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2reu8i.x 
 |-  ( x = v -> ( ph <-> ta ) )
2 2reu8i.v 
 |-  ( x = v -> ( ch <-> th ) )
3 2reu8i.w 
 |-  ( y = w -> ( ph <-> ch ) )
4 2reu8i.b 
 |-  ( y = b -> ( ph <-> et ) )
5 2reu8i.a 
 |-  ( x = a -> ( ch <-> ze ) )
6 2reu8i.1 
 |-  ( ( ( ch -> y = w ) /\ ze ) -> y = w )
7 2reu8i.2 
 |-  ( ( x = a /\ y = b ) -> ( ph <-> ps ) )
8 3 reu8 
 |-  ( E! y e. B ph <-> E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) )
9 8 reubii 
 |-  ( E! x e. A E! y e. B ph <-> E! x e. A E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) )
10 2 imbi1d 
 |-  ( x = v -> ( ( ch -> y = w ) <-> ( th -> y = w ) ) )
11 10 ralbidv 
 |-  ( x = v -> ( A. w e. B ( ch -> y = w ) <-> A. w e. B ( th -> y = w ) ) )
12 1 11 anbi12d 
 |-  ( x = v -> ( ( ph /\ A. w e. B ( ch -> y = w ) ) <-> ( ta /\ A. w e. B ( th -> y = w ) ) ) )
13 12 rexbidv 
 |-  ( x = v -> ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) <-> E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) ) )
14 13 reu8 
 |-  ( E! x e. A E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) <-> E. x e. A ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) -> x = v ) ) )
15 9 14 bitri 
 |-  ( E! x e. A E! y e. B ph <-> E. x e. A ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) -> x = v ) ) )
16 nfv 
 |-  F/ u ( ta /\ A. w e. B ( th -> y = w ) )
17 nfs1v 
 |-  F/ y [ u / y ] ta
18 nfcv 
 |-  F/_ y B
19 nfs1v 
 |-  F/ y [ u / y ] th
20 nfv 
 |-  F/ y u = w
21 19 20 nfim 
 |-  F/ y ( [ u / y ] th -> u = w )
22 18 21 nfralw 
 |-  F/ y A. w e. B ( [ u / y ] th -> u = w )
23 17 22 nfan 
 |-  F/ y ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) )
24 sbequ12 
 |-  ( y = u -> ( ta <-> [ u / y ] ta ) )
25 sbequ12 
 |-  ( y = u -> ( th <-> [ u / y ] th ) )
26 equequ1 
 |-  ( y = u -> ( y = w <-> u = w ) )
27 25 26 imbi12d 
 |-  ( y = u -> ( ( th -> y = w ) <-> ( [ u / y ] th -> u = w ) ) )
28 27 ralbidv 
 |-  ( y = u -> ( A. w e. B ( th -> y = w ) <-> A. w e. B ( [ u / y ] th -> u = w ) ) )
29 24 28 anbi12d 
 |-  ( y = u -> ( ( ta /\ A. w e. B ( th -> y = w ) ) <-> ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) ) )
30 16 23 29 cbvrexw 
 |-  ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) <-> E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) )
31 30 imbi1i 
 |-  ( ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) -> x = v ) <-> ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) )
32 31 ralbii 
 |-  ( A. v e. A ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) -> x = v ) <-> A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) )
33 32 anbi2i 
 |-  ( ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) -> x = v ) ) <-> ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) )
34 nfcv 
 |-  F/_ y A
35 18 23 nfrex 
 |-  F/ y E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) )
36 nfv 
 |-  F/ y x = v
37 35 36 nfim 
 |-  F/ y ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v )
38 34 37 nfralw 
 |-  F/ y A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v )
39 38 r19.41 
 |-  ( E. y e. B ( ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) <-> ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) )
40 33 39 bitr4i 
 |-  ( ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) -> x = v ) ) <-> E. y e. B ( ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) )
41 r19.28v 
 |-  ( ( A. w e. B ( ch -> y = w ) /\ A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) -> A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) )
42 simplr 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) ) -> ph )
43 nfv 
 |-  F/ v A. w e. B ( ch -> y = w )
44 nfcv 
 |-  F/_ v B
45 nfs1v 
 |-  F/ v [ a / v ] [ u / y ] ta
46 nfs1v 
 |-  F/ v [ a / v ] [ u / y ] th
47 nfv 
 |-  F/ v u = w
48 46 47 nfim 
 |-  F/ v ( [ a / v ] [ u / y ] th -> u = w )
49 44 48 nfralw 
 |-  F/ v A. w e. B ( [ a / v ] [ u / y ] th -> u = w )
50 45 49 nfan 
 |-  F/ v ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) )
51 44 50 nfrex 
 |-  F/ v E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) )
52 nfv 
 |-  F/ v x = a
53 51 52 nfim 
 |-  F/ v ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a )
54 43 53 nfan 
 |-  F/ v ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) )
55 sbequ12 
 |-  ( v = a -> ( [ u / y ] ta <-> [ a / v ] [ u / y ] ta ) )
56 sbequ12 
 |-  ( v = a -> ( [ u / y ] th <-> [ a / v ] [ u / y ] th ) )
57 56 imbi1d 
 |-  ( v = a -> ( ( [ u / y ] th -> u = w ) <-> ( [ a / v ] [ u / y ] th -> u = w ) ) )
58 57 ralbidv 
 |-  ( v = a -> ( A. w e. B ( [ u / y ] th -> u = w ) <-> A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) )
59 55 58 anbi12d 
 |-  ( v = a -> ( ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) <-> ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) ) )
60 59 rexbidv 
 |-  ( v = a -> ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) <-> E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) ) )
61 equequ2 
 |-  ( v = a -> ( x = v <-> x = a ) )
62 60 61 imbi12d 
 |-  ( v = a -> ( ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) <-> ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) )
63 62 anbi2d 
 |-  ( v = a -> ( ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) <-> ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) ) )
64 54 63 rspc 
 |-  ( a e. A -> ( A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) -> ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) ) )
65 64 ad2antrl 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) -> ( A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) -> ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) ) )
66 nfs1v 
 |-  F/ w [ b / w ] ch
67 nfv 
 |-  F/ w y = b
68 66 67 nfim 
 |-  F/ w ( [ b / w ] ch -> y = b )
69 sbequ12 
 |-  ( w = b -> ( ch <-> [ b / w ] ch ) )
70 equequ2 
 |-  ( w = b -> ( y = w <-> y = b ) )
71 69 70 imbi12d 
 |-  ( w = b -> ( ( ch -> y = w ) <-> ( [ b / w ] ch -> y = b ) ) )
72 68 71 rspc 
 |-  ( b e. B -> ( A. w e. B ( ch -> y = w ) -> ( [ b / w ] ch -> y = b ) ) )
73 72 adantl 
 |-  ( ( a e. A /\ b e. B ) -> ( A. w e. B ( ch -> y = w ) -> ( [ b / w ] ch -> y = b ) ) )
74 73 adantl 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) -> ( A. w e. B ( ch -> y = w ) -> ( [ b / w ] ch -> y = b ) ) )
75 74 imp 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) -> ( [ b / w ] ch -> y = b ) )
76 3 sbievw 
 |-  ( [ w / y ] ph <-> ch )
77 76 bicomi 
 |-  ( ch <-> [ w / y ] ph )
78 77 sbbii 
 |-  ( [ b / w ] ch <-> [ b / w ] [ w / y ] ph )
79 sbco2vv 
 |-  ( [ b / w ] [ w / y ] ph <-> [ b / y ] ph )
80 78 79 bitri 
 |-  ( [ b / w ] ch <-> [ b / y ] ph )
81 80 imbi1i 
 |-  ( ( [ b / w ] ch -> y = b ) <-> ( [ b / y ] ph -> y = b ) )
82 4 sbievw 
 |-  ( [ b / y ] ph <-> et )
83 pm3.35 
 |-  ( ( [ b / y ] ph /\ ( [ b / y ] ph -> y = b ) ) -> y = b )
84 83 equcomd 
 |-  ( ( [ b / y ] ph /\ ( [ b / y ] ph -> y = b ) ) -> b = y )
85 84 ex 
 |-  ( [ b / y ] ph -> ( ( [ b / y ] ph -> y = b ) -> b = y ) )
86 82 85 sylbir 
 |-  ( et -> ( ( [ b / y ] ph -> y = b ) -> b = y ) )
87 86 com12 
 |-  ( ( [ b / y ] ph -> y = b ) -> ( et -> b = y ) )
88 87 ad2antlr 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) -> ( et -> b = y ) )
89 simplrr 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) -> b e. B )
90 89 ad2antrr 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) -> b e. B )
91 sbequ 
 |-  ( u = b -> ( [ u / y ] ph <-> [ b / y ] ph ) )
92 91 sbbidv 
 |-  ( u = b -> ( [ a / x ] [ u / y ] ph <-> [ a / x ] [ b / y ] ph ) )
93 equequ1 
 |-  ( u = b -> ( u = w <-> b = w ) )
94 93 imbi2d 
 |-  ( u = b -> ( ( [ a / x ] [ w / y ] ph -> u = w ) <-> ( [ a / x ] [ w / y ] ph -> b = w ) ) )
95 94 ralbidv 
 |-  ( u = b -> ( A. w e. B ( [ a / x ] [ w / y ] ph -> u = w ) <-> A. w e. B ( [ a / x ] [ w / y ] ph -> b = w ) ) )
96 92 95 anbi12d 
 |-  ( u = b -> ( ( [ a / x ] [ u / y ] ph /\ A. w e. B ( [ a / x ] [ w / y ] ph -> u = w ) ) <-> ( [ a / x ] [ b / y ] ph /\ A. w e. B ( [ a / x ] [ w / y ] ph -> b = w ) ) ) )
97 96 adantl 
 |-  ( ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) /\ u = b ) -> ( ( [ a / x ] [ u / y ] ph /\ A. w e. B ( [ a / x ] [ w / y ] ph -> u = w ) ) <-> ( [ a / x ] [ b / y ] ph /\ A. w e. B ( [ a / x ] [ w / y ] ph -> b = w ) ) ) )
98 vex 
 |-  a e. _V
99 vex 
 |-  b e. _V
100 98 99 7 sbc2ie 
 |-  ( [. a / x ]. [. b / y ]. ph <-> ps )
101 100 a1i 
 |-  ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) -> ( [. a / x ]. [. b / y ]. ph <-> ps ) )
102 101 biimprd 
 |-  ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) -> ( ps -> [. a / x ]. [. b / y ]. ph ) )
103 102 adantld 
 |-  ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) -> ( ( et /\ ps ) -> [. a / x ]. [. b / y ]. ph ) )
104 103 imp 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) -> [. a / x ]. [. b / y ]. ph )
105 sbsbc 
 |-  ( [ b / y ] ph <-> [. b / y ]. ph )
106 105 sbbii 
 |-  ( [ a / x ] [ b / y ] ph <-> [ a / x ] [. b / y ]. ph )
107 sbsbc 
 |-  ( [ a / x ] [. b / y ]. ph <-> [. a / x ]. [. b / y ]. ph )
108 106 107 bitri 
 |-  ( [ a / x ] [ b / y ] ph <-> [. a / x ]. [. b / y ]. ph )
109 104 108 sylibr 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) -> [ a / x ] [ b / y ] ph )
110 76 sbbii 
 |-  ( [ a / x ] [ w / y ] ph <-> [ a / x ] ch )
111 5 sbievw 
 |-  ( [ a / x ] ch <-> ze )
112 110 111 bitri 
 |-  ( [ a / x ] [ w / y ] ph <-> ze )
113 6 ex 
 |-  ( ( ch -> y = w ) -> ( ze -> y = w ) )
114 113 adantl 
 |-  ( ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ w e. B ) /\ ( ch -> y = w ) ) -> ( ze -> y = w ) )
115 82 imbi1i 
 |-  ( ( [ b / y ] ph -> y = b ) <-> ( et -> y = b ) )
116 pm2.27 
 |-  ( et -> ( ( et -> y = b ) -> y = b ) )
117 116 ad2antrl 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) -> ( ( et -> y = b ) -> y = b ) )
118 115 117 syl5bi 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) -> ( ( [ b / y ] ph -> y = b ) -> y = b ) )
119 ax7 
 |-  ( y = b -> ( y = w -> b = w ) )
120 118 119 syl6 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) -> ( ( [ b / y ] ph -> y = b ) -> ( y = w -> b = w ) ) )
121 120 imp 
 |-  ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) /\ ( [ b / y ] ph -> y = b ) ) -> ( y = w -> b = w ) )
122 121 ad2antrr 
 |-  ( ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ w e. B ) /\ ( ch -> y = w ) ) -> ( y = w -> b = w ) )
123 114 122 syld 
 |-  ( ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ w e. B ) /\ ( ch -> y = w ) ) -> ( ze -> b = w ) )
124 112 123 syl5bi 
 |-  ( ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ w e. B ) /\ ( ch -> y = w ) ) -> ( [ a / x ] [ w / y ] ph -> b = w ) )
125 124 ex 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ w e. B ) -> ( ( ch -> y = w ) -> ( [ a / x ] [ w / y ] ph -> b = w ) ) )
126 125 ralimdva 
 |-  ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ ( et /\ ps ) ) /\ ( [ b / y ] ph -> y = b ) ) -> ( A. w e. B ( ch -> y = w ) -> A. w e. B ( [ a / x ] [ w / y ] ph -> b = w ) ) )
127 126 exp31 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) -> ( ( et /\ ps ) -> ( ( [ b / y ] ph -> y = b ) -> ( A. w e. B ( ch -> y = w ) -> A. w e. B ( [ a / x ] [ w / y ] ph -> b = w ) ) ) ) )
128 127 com24 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) -> ( A. w e. B ( ch -> y = w ) -> ( ( [ b / y ] ph -> y = b ) -> ( ( et /\ ps ) -> A. w e. B ( [ a / x ] [ w / y ] ph -> b = w ) ) ) ) )
129 128 imp41 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) -> A. w e. B ( [ a / x ] [ w / y ] ph -> b = w ) )
130 109 129 jca 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) -> ( [ a / x ] [ b / y ] ph /\ A. w e. B ( [ a / x ] [ w / y ] ph -> b = w ) ) )
131 90 97 130 rspcedvd 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) -> E. u e. B ( [ a / x ] [ u / y ] ph /\ A. w e. B ( [ a / x ] [ w / y ] ph -> u = w ) ) )
132 1 sbievw 
 |-  ( [ v / x ] ph <-> ta )
133 132 bicomi 
 |-  ( ta <-> [ v / x ] ph )
134 133 sbbii 
 |-  ( [ u / y ] ta <-> [ u / y ] [ v / x ] ph )
135 sbcom2 
 |-  ( [ u / y ] [ v / x ] ph <-> [ v / x ] [ u / y ] ph )
136 134 135 bitri 
 |-  ( [ u / y ] ta <-> [ v / x ] [ u / y ] ph )
137 136 sbbii 
 |-  ( [ a / v ] [ u / y ] ta <-> [ a / v ] [ v / x ] [ u / y ] ph )
138 sbco2vv 
 |-  ( [ a / v ] [ v / x ] [ u / y ] ph <-> [ a / x ] [ u / y ] ph )
139 137 138 bitri 
 |-  ( [ a / v ] [ u / y ] ta <-> [ a / x ] [ u / y ] ph )
140 2 sbievw 
 |-  ( [ v / x ] ch <-> th )
141 140 bicomi 
 |-  ( th <-> [ v / x ] ch )
142 141 sbbii 
 |-  ( [ u / y ] th <-> [ u / y ] [ v / x ] ch )
143 sbcom2 
 |-  ( [ u / y ] [ v / x ] ch <-> [ v / x ] [ u / y ] ch )
144 142 143 bitri 
 |-  ( [ u / y ] th <-> [ v / x ] [ u / y ] ch )
145 144 sbbii 
 |-  ( [ a / v ] [ u / y ] th <-> [ a / v ] [ v / x ] [ u / y ] ch )
146 sbco2vv 
 |-  ( [ a / v ] [ v / x ] [ u / y ] ch <-> [ a / x ] [ u / y ] ch )
147 77 sbbii 
 |-  ( [ u / y ] ch <-> [ u / y ] [ w / y ] ph )
148 nfs1v 
 |-  F/ y [ w / y ] ph
149 148 sbf 
 |-  ( [ u / y ] [ w / y ] ph <-> [ w / y ] ph )
150 147 149 bitri 
 |-  ( [ u / y ] ch <-> [ w / y ] ph )
151 150 sbbii 
 |-  ( [ a / x ] [ u / y ] ch <-> [ a / x ] [ w / y ] ph )
152 145 146 151 3bitri 
 |-  ( [ a / v ] [ u / y ] th <-> [ a / x ] [ w / y ] ph )
153 152 imbi1i 
 |-  ( ( [ a / v ] [ u / y ] th -> u = w ) <-> ( [ a / x ] [ w / y ] ph -> u = w ) )
154 153 ralbii 
 |-  ( A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) <-> A. w e. B ( [ a / x ] [ w / y ] ph -> u = w ) )
155 139 154 anbi12i 
 |-  ( ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) <-> ( [ a / x ] [ u / y ] ph /\ A. w e. B ( [ a / x ] [ w / y ] ph -> u = w ) ) )
156 155 rexbii 
 |-  ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) <-> E. u e. B ( [ a / x ] [ u / y ] ph /\ A. w e. B ( [ a / x ] [ w / y ] ph -> u = w ) ) )
157 131 156 sylibr 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) -> E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) )
158 pm2.27 
 |-  ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> ( ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) -> x = a ) )
159 157 158 syl 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( et /\ ps ) ) -> ( ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) -> x = a ) )
160 159 impancom 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) -> ( ( et /\ ps ) -> x = a ) )
161 160 imp 
 |-  ( ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) /\ ( et /\ ps ) ) -> x = a )
162 161 equcomd 
 |-  ( ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) /\ ( et /\ ps ) ) -> a = x )
163 162 exp32 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) -> ( et -> ( ps -> a = x ) ) )
164 88 163 jcad 
 |-  ( ( ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) /\ ( [ b / y ] ph -> y = b ) ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) -> ( et -> ( b = y /\ ( ps -> a = x ) ) ) )
165 164 exp31 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) -> ( ( [ b / y ] ph -> y = b ) -> ( ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) -> ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) )
166 81 165 syl5bi 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) -> ( ( [ b / w ] ch -> y = b ) -> ( ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) -> ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) )
167 75 166 mpd 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) /\ A. w e. B ( ch -> y = w ) ) -> ( ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) -> ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) )
168 167 expimpd 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) -> ( ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ a / v ] [ u / y ] ta /\ A. w e. B ( [ a / v ] [ u / y ] th -> u = w ) ) -> x = a ) ) -> ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) )
169 65 168 syld 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ ( a e. A /\ b e. B ) ) -> ( A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) -> ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) )
170 169 impancom 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) ) -> ( ( a e. A /\ b e. B ) -> ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) )
171 170 ralrimivv 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) ) -> A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) )
172 42 171 jca 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ph ) /\ A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) ) -> ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) )
173 172 ex 
 |-  ( ( ( x e. A /\ y e. B ) /\ ph ) -> ( A. v e. A ( A. w e. B ( ch -> y = w ) /\ ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) -> ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) )
174 41 173 syl5 
 |-  ( ( ( x e. A /\ y e. B ) /\ ph ) -> ( ( A. w e. B ( ch -> y = w ) /\ A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) -> ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) )
175 174 expd 
 |-  ( ( ( x e. A /\ y e. B ) /\ ph ) -> ( A. w e. B ( ch -> y = w ) -> ( A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) -> ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) ) )
176 175 expimpd 
 |-  ( ( x e. A /\ y e. B ) -> ( ( ph /\ A. w e. B ( ch -> y = w ) ) -> ( A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) -> ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) ) )
177 176 impd 
 |-  ( ( x e. A /\ y e. B ) -> ( ( ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) -> ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) )
178 177 reximdva 
 |-  ( x e. A -> ( E. y e. B ( ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. u e. B ( [ u / y ] ta /\ A. w e. B ( [ u / y ] th -> u = w ) ) -> x = v ) ) -> E. y e. B ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) )
179 40 178 syl5bi 
 |-  ( x e. A -> ( ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) -> x = v ) ) -> E. y e. B ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) ) )
180 179 reximia 
 |-  ( E. x e. A ( E. y e. B ( ph /\ A. w e. B ( ch -> y = w ) ) /\ A. v e. A ( E. y e. B ( ta /\ A. w e. B ( th -> y = w ) ) -> x = v ) ) -> E. x e. A E. y e. B ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) )
181 15 180 sylbi 
 |-  ( E! x e. A E! y e. B ph -> E. x e. A E. y e. B ( ph /\ A. a e. A A. b e. B ( et -> ( b = y /\ ( ps -> a = x ) ) ) ) )