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→φ↔τ
2reu8i.v ⊢x=v→χ↔θ
2reu8i.w ⊢y=w→φ↔χ
2reu8i.b ⊢y=b→φ↔η
2reu8i.a ⊢x=a→χ↔ζ
2reu8i.1 ⊢χ→y=w∧ζ→y=w
2reu8i.2 ⊢x=a∧y=b→φ↔ψ
Assertion 2reu8i ⊢∃!x∈A∃!y∈Bφ→∃x∈A∃y∈Bφ∧∀a∈A∀b∈Bη→b=y∧ψ→a=x

Proof

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