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 ⊢ Ⅎ y u y τ
18 nfcv ⊢ Ⅎ _ y B
19 nfs1v ⊢ Ⅎ y u y θ
20 nfv ⊢ Ⅎ y u = w
21 19 20 nfim ⊢ Ⅎ y u y θ → u = w
22 18 21 nfralw ⊢ Ⅎ y ∀ w ∈ B u y θ → u = w
23 17 22 nfan ⊢ Ⅎ y u y τ ∧ ∀ w ∈ B u y θ → u = w
24 sbequ12 ⊢ y = u → τ ↔ u y τ
25 sbequ12 ⊢ y = u → θ ↔ u y θ
26 equequ1 ⊢ y = u → y = w ↔ u = w
27 25 26 imbi12d ⊢ y = u → θ → y = w ↔ u y θ → u = w
28 27 ralbidv ⊢ y = u → ∀ w ∈ B θ → y = w ↔ ∀ w ∈ B u y θ → u = w
29 24 28 anbi12d ⊢ y = u → τ ∧ ∀ w ∈ B θ → y = w ↔ u y τ ∧ ∀ w ∈ B u y θ → u = w
30 16 23 29 cbvrexw ⊢ ∃ y ∈ B τ ∧ ∀ w ∈ B θ → y = w ↔ ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w
31 30 imbi1i ⊢ ∃ y ∈ B τ ∧ ∀ w ∈ B θ → y = w → x = v ↔ ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v
32 31 ralbii ⊢ ∀ v ∈ A ∃ y ∈ B τ ∧ ∀ w ∈ B θ → y = w → x = v ↔ ∀ v ∈ A ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v
34 nfcv ⊢ Ⅎ _ y A
35 18 23 nfrex ⊢ Ⅎ y ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w
36 nfv ⊢ Ⅎ y x = v
37 35 36 nfim ⊢ Ⅎ y ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v
38 34 37 nfralw ⊢ Ⅎ y ∀ v ∈ A ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v
39 38 r19.41 ⊢ ∃ y ∈ B φ ∧ ∀ w ∈ B χ → y = w ∧ ∀ v ∈ A ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v ↔ ∃ y ∈ B φ ∧ ∀ w ∈ B χ → y = w ∧ ∀ v ∈ A ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v
41 r19.28v ⊢ ∀ w ∈ B χ → y = w ∧ ∀ v ∈ A ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v → ∀ v ∈ A ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v
42 simplr ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ ∀ v ∈ A ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v → φ
43 nfv ⊢ Ⅎ v ∀ w ∈ B χ → y = w
44 nfcv ⊢ Ⅎ _ v B
45 nfs1v ⊢ Ⅎ v a v u y τ
46 nfs1v ⊢ Ⅎ v a v u y θ
47 nfv ⊢ Ⅎ v u = w
48 46 47 nfim ⊢ Ⅎ v a v u y θ → u = w
49 44 48 nfralw ⊢ Ⅎ v ∀ w ∈ B a v u y θ → u = w
50 45 49 nfan ⊢ Ⅎ v a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w
51 44 50 nfrex ⊢ Ⅎ v ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w
52 nfv ⊢ Ⅎ v x = a
53 51 52 nfim ⊢ Ⅎ v ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a
54 43 53 nfan ⊢ Ⅎ v ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a
55 sbequ12 ⊢ v = a → u y τ ↔ a v u y τ
56 sbequ12 ⊢ v = a → u y θ ↔ a v u y θ
57 56 imbi1d ⊢ v = a → u y θ → u = w ↔ a v u y θ → u = w
58 57 ralbidv ⊢ v = a → ∀ w ∈ B u y θ → u = w ↔ ∀ w ∈ B a v u y θ → u = w
59 55 58 anbi12d ⊢ v = a → u y τ ∧ ∀ w ∈ B u y θ → u = w ↔ a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w
60 59 rexbidv ⊢ v = a → ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w ↔ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w
61 equequ2 ⊢ v = a → x = v ↔ x = a
62 60 61 imbi12d ⊢ v = a → ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v ↔ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a
63 62 anbi2d ⊢ v = a → ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v ↔ ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a
64 54 63 rspc ⊢ a ∈ A → ∀ v ∈ A ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v → ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a
65 64 ad2antrl ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B → ∀ v ∈ A ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v → ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a
66 nfs1v ⊢ Ⅎ w b w χ
67 nfv ⊢ Ⅎ w y = b
68 66 67 nfim ⊢ Ⅎ w b w χ → y = b
69 sbequ12 ⊢ w = b → χ ↔ b w χ
70 equequ2 ⊢ w = b → y = w ↔ y = b
71 69 70 imbi12d ⊢ w = b → χ → y = w ↔ b w χ → y = b
72 68 71 rspc ⊢ b ∈ B → ∀ w ∈ B χ → y = w → b w χ → y = b
73 72 adantl ⊢ a ∈ A ∧ b ∈ B → ∀ w ∈ B χ → y = w → b w χ → y = b
74 73 adantl ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B → ∀ w ∈ B χ → y = w → b w χ → y = b
75 74 imp ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w → b w χ → y = b
76 3 sbievw ⊢ w y φ ↔ χ
77 76 bicomi ⊢ χ ↔ w y φ
78 77 sbbii ⊢ b w χ ↔ b w w y φ
79 sbco2vv ⊢ b w w y φ ↔ b y φ
80 78 79 bitri ⊢ b w χ ↔ b y φ
81 80 imbi1i ⊢ b w χ → y = b ↔ b y φ → y = b
82 4 sbievw ⊢ b y φ ↔ η
83 pm3.35 ⊢ b y φ ∧ b y φ → y = b → y = b
84 83 equcomd ⊢ b y φ ∧ b y φ → y = b → b = y
85 84 ex ⊢ b y φ → b y φ → y = b → b = y
86 82 85 sylbir ⊢ η → b y φ → y = b → b = y
87 86 com12 ⊢ b y φ → y = b → η → b = y
88 87 ad2antlr ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → 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 ∧ b y φ → y = b ∧ η ∧ ψ → b ∈ B
91 sbequ ⊢ u = b → u y φ ↔ b y φ
92 91 sbbidv ⊢ u = b → a x u y φ ↔ a x b y φ
93 equequ1 ⊢ u = b → u = w ↔ b = w
94 93 imbi2d ⊢ u = b → a x w y φ → u = w ↔ a x w y φ → b = w
95 94 ralbidv ⊢ u = b → ∀ w ∈ B a x w y φ → u = w ↔ ∀ w ∈ B a x w y φ → b = w
96 92 95 anbi12d ⊢ u = b → a x u y φ ∧ ∀ w ∈ B a x w y φ → u = w ↔ a x b y φ ∧ ∀ w ∈ B a x w y φ → b = w
97 96 adantl ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ η ∧ ψ ∧ u = b → a x u y φ ∧ ∀ w ∈ B a x w y φ → u = w ↔ a x b y φ ∧ ∀ w ∈ B a x w y φ → 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 ∧ b y φ → y = b → [˙a / x]˙ [˙b / y]˙ φ ↔ ψ
102 101 biimprd ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b → ψ → [˙a / x]˙ [˙b / y]˙ φ
103 102 adantld ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b → η ∧ ψ → [˙a / x]˙ [˙b / y]˙ φ
104 103 imp ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ η ∧ ψ → [˙a / x]˙ [˙b / y]˙ φ
105 sbsbc ⊢ b y φ ↔ [˙b / y]˙ φ
106 105 sbbii ⊢ a x b y φ ↔ a x [˙b / y]˙ φ
107 sbsbc ⊢ a x [˙b / y]˙ φ ↔ [˙a / x]˙ [˙b / y]˙ φ
108 106 107 bitri ⊢ a x b y φ ↔ [˙a / x]˙ [˙b / y]˙ φ
109 104 108 sylibr ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ η ∧ ψ → a x b y φ
110 76 sbbii ⊢ a x w y φ ↔ a x χ
111 5 sbievw ⊢ a x χ ↔ ζ
112 110 111 bitri ⊢ a x w y φ ↔ ζ
113 6 ex ⊢ χ → y = w → ζ → y = w
114 113 adantl ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ ∧ b y φ → y = b ∧ w ∈ B ∧ χ → y = w → ζ → y = w
115 82 imbi1i ⊢ b y φ → 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 syl5bi ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ → b y φ → y = b → y = b
119 ax7 ⊢ y = b → y = w → b = w
120 118 119 syl6 ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ → b y φ → y = b → y = w → b = w
121 120 imp ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ ∧ b y φ → y = b → y = w → b = w
122 121 ad2antrr ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ ∧ b y φ → y = b ∧ w ∈ B ∧ χ → y = w → y = w → b = w
123 114 122 syld ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ ∧ b y φ → y = b ∧ w ∈ B ∧ χ → y = w → ζ → b = w
124 112 123 syl5bi ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ ∧ b y φ → y = b ∧ w ∈ B ∧ χ → y = w → a x w y φ → b = w
125 124 ex ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ ∧ b y φ → y = b ∧ w ∈ B → χ → y = w → a x w y φ → b = w
126 125 ralimdva ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ η ∧ ψ ∧ b y φ → y = b → ∀ w ∈ B χ → y = w → ∀ w ∈ B a x w y φ → b = w
127 126 exp31 ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B → η ∧ ψ → b y φ → y = b → ∀ w ∈ B χ → y = w → ∀ w ∈ B a x w y φ → b = w
128 127 com24 ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B → ∀ w ∈ B χ → y = w → b y φ → y = b → η ∧ ψ → ∀ w ∈ B a x w y φ → b = w
129 128 imp41 ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ η ∧ ψ → ∀ w ∈ B a x w y φ → b = w
130 109 129 jca ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ η ∧ ψ → a x b y φ ∧ ∀ w ∈ B a x w y φ → b = w
131 90 97 130 rspcedvd ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ η ∧ ψ → ∃ u ∈ B a x u y φ ∧ ∀ w ∈ B a x w y φ → u = w
132 1 sbievw ⊢ v x φ ↔ τ
133 132 bicomi ⊢ τ ↔ v x φ
134 133 sbbii ⊢ u y τ ↔ u y v x φ
135 sbcom2 ⊢ u y v x φ ↔ v x u y φ
136 134 135 bitri ⊢ u y τ ↔ v x u y φ
137 136 sbbii ⊢ a v u y τ ↔ a v v x u y φ
138 sbco2vv ⊢ a v v x u y φ ↔ a x u y φ
139 137 138 bitri ⊢ a v u y τ ↔ a x u y φ
140 2 sbievw ⊢ v x χ ↔ θ
141 140 bicomi ⊢ θ ↔ v x χ
142 141 sbbii ⊢ u y θ ↔ u y v x χ
143 sbcom2 ⊢ u y v x χ ↔ v x u y χ
144 142 143 bitri ⊢ u y θ ↔ v x u y χ
145 144 sbbii ⊢ a v u y θ ↔ a v v x u y χ
146 sbco2vv ⊢ a v v x u y χ ↔ a x u y χ
147 77 sbbii ⊢ u y χ ↔ u y w y φ
148 nfs1v ⊢ Ⅎ y w y φ
149 148 sbf ⊢ u y w y φ ↔ w y φ
150 147 149 bitri ⊢ u y χ ↔ w y φ
151 150 sbbii ⊢ a x u y χ ↔ a x w y φ
152 145 146 151 3bitri ⊢ a v u y θ ↔ a x w y φ
153 152 imbi1i ⊢ a v u y θ → u = w ↔ a x w y φ → u = w
154 153 ralbii ⊢ ∀ w ∈ B a v u y θ → u = w ↔ ∀ w ∈ B a x w y φ → u = w
155 139 154 anbi12i ⊢ a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w ↔ a x u y φ ∧ ∀ w ∈ B a x w y φ → u = w
156 155 rexbii ⊢ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w ↔ ∃ u ∈ B a x u y φ ∧ ∀ w ∈ B a x w y φ → u = w
157 131 156 sylibr ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ η ∧ ψ → ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w
158 pm2.27 ⊢ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a → x = a
159 157 158 syl ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ η ∧ ψ → ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a → x = a
160 159 impancom ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a → η ∧ ψ → x = a
161 160 imp ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a ∧ η ∧ ψ → x = a
162 161 equcomd ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a ∧ η ∧ ψ → a = x
163 162 exp32 ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a → η → ψ → a = x
164 88 163 jcad ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w ∧ b y φ → y = b ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a → η → b = y ∧ ψ → a = x
165 164 exp31 ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w → b y φ → y = b → ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a → η → b = y ∧ ψ → a = x
166 81 165 syl5bi ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B ∧ ∀ w ∈ B χ → y = w → b w χ → y = b → ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → 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 ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → u = w → x = a → η → b = y ∧ ψ → a = x
168 167 expimpd ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ a ∈ A ∧ b ∈ B → ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B a v u y τ ∧ ∀ w ∈ B a v u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v → η → b = y ∧ ψ → a = x
170 169 impancom ⊢ x ∈ A ∧ y ∈ B ∧ φ ∧ ∀ v ∈ A ∀ w ∈ B χ → y = w ∧ ∃ u ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → 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 ∈ B u y τ ∧ ∀ w ∈ B u y θ → u = w → x = v → ∃ y ∈ B φ ∧ ∀ a ∈ A ∀ b ∈ B η → b = y ∧ ψ → a = x
179 40 178 syl5bi ⊢ 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