Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2reu8i Structured version   Visualization version   GIF version

Theorem 2reu8i 42168
Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 42167. 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.)
Hypotheses
Ref Expression
2reu8i.x (𝑥 = 𝑣 → (𝜑𝜏))
2reu8i.v (𝑥 = 𝑣 → (𝜒𝜃))
2reu8i.w (𝑦 = 𝑤 → (𝜑𝜒))
2reu8i.b (𝑦 = 𝑏 → (𝜑𝜂))
2reu8i.a (𝑥 = 𝑎 → (𝜒𝜁))
2reu8i.1 (((𝜒𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤)
2reu8i.2 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑𝜓))
Assertion
Ref Expression
2reu8i (∃!𝑥𝐴 ∃!𝑦𝐵 𝜑 → ∃𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑣,𝑤,𝑥,𝑦   𝐵,𝑎,𝑏,𝑣,𝑤,𝑥,𝑦   𝜑,𝑎,𝑏,𝑣,𝑤   𝜒,𝑎,𝑏,𝑣,𝑦   𝜏,𝑎,𝑏,𝑥   𝜃,𝑎,𝑏,𝑥   𝜂,𝑤,𝑦   𝜓,𝑤,𝑥,𝑦   𝜁,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑣,𝑎,𝑏)   𝜒(𝑥,𝑤)   𝜃(𝑦,𝑤,𝑣)   𝜏(𝑦,𝑤,𝑣)   𝜂(𝑥,𝑣,𝑎,𝑏)   𝜁(𝑦,𝑤,𝑣,𝑎,𝑏)

Proof of Theorem 2reu8i
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 2reu8i.w . . . . 5 (𝑦 = 𝑤 → (𝜑𝜒))
21reu8 3614 . . . 4 (∃!𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)))
32reubii 3316 . . 3 (∃!𝑥𝐴 ∃!𝑦𝐵 𝜑 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)))
4 2reu8i.x . . . . . 6 (𝑥 = 𝑣 → (𝜑𝜏))
5 2reu8i.v . . . . . . . 8 (𝑥 = 𝑣 → (𝜒𝜃))
65imbi1d 333 . . . . . . 7 (𝑥 = 𝑣 → ((𝜒𝑦 = 𝑤) ↔ (𝜃𝑦 = 𝑤)))
76ralbidv 3168 . . . . . 6 (𝑥 = 𝑣 → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ↔ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)))
84, 7anbi12d 624 . . . . 5 (𝑥 = 𝑣 → ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ↔ (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤))))
98rexbidv 3237 . . . 4 (𝑥 = 𝑣 → (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ↔ ∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤))))
109reu8 3614 . . 3 (∃!𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ↔ ∃𝑥𝐴 (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)))
113, 10bitri 267 . 2 (∃!𝑥𝐴 ∃!𝑦𝐵 𝜑 ↔ ∃𝑥𝐴 (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)))
12 nfv 1957 . . . . . . . . 9 𝑢(𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤))
13 nfs1v 2254 . . . . . . . . . 10 𝑦[𝑢 / 𝑦]𝜏
14 nfcv 2934 . . . . . . . . . . 11 𝑦𝐵
15 nfs1v 2254 . . . . . . . . . . . 12 𝑦[𝑢 / 𝑦]𝜃
16 nfv 1957 . . . . . . . . . . . 12 𝑦 𝑢 = 𝑤
1715, 16nfim 1943 . . . . . . . . . . 11 𝑦([𝑢 / 𝑦]𝜃𝑢 = 𝑤)
1814, 17nfral 3127 . . . . . . . . . 10 𝑦𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)
1913, 18nfan 1946 . . . . . . . . 9 𝑦([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤))
20 sbequ12 2229 . . . . . . . . . 10 (𝑦 = 𝑢 → (𝜏 ↔ [𝑢 / 𝑦]𝜏))
21 sbequ12 2229 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝜃 ↔ [𝑢 / 𝑦]𝜃))
22 equequ1 2072 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑦 = 𝑤𝑢 = 𝑤))
2321, 22imbi12d 336 . . . . . . . . . . 11 (𝑦 = 𝑢 → ((𝜃𝑦 = 𝑤) ↔ ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
2423ralbidv 3168 . . . . . . . . . 10 (𝑦 = 𝑢 → (∀𝑤𝐵 (𝜃𝑦 = 𝑤) ↔ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
2520, 24anbi12d 624 . . . . . . . . 9 (𝑦 = 𝑢 → ((𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) ↔ ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤))))
2612, 19, 25cbvrex 3364 . . . . . . . 8 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) ↔ ∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
2726imbi1i 341 . . . . . . 7 ((∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))
2827ralbii 3162 . . . . . 6 (∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))
2928anbi2i 616 . . . . 5 ((∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)))
30 nfcv 2934 . . . . . . 7 𝑦𝐴
3114, 19nfrex 3188 . . . . . . . 8 𝑦𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤))
32 nfv 1957 . . . . . . . 8 𝑦 𝑥 = 𝑣
3331, 32nfim 1943 . . . . . . 7 𝑦(∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)
3430, 33nfral 3127 . . . . . 6 𝑦𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)
3534r19.41 3276 . . . . 5 (∃𝑦𝐵 ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)))
3629, 35bitr4i 270 . . . 4 ((∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ ∃𝑦𝐵 ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)))
37 r19.28v 3257 . . . . . . . . 9 ((∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)))
38 simplr 759 . . . . . . . . . . 11 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))) → 𝜑)
39 nfv 1957 . . . . . . . . . . . . . . . . 17 𝑣𝑤𝐵 (𝜒𝑦 = 𝑤)
40 nfcv 2934 . . . . . . . . . . . . . . . . . . 19 𝑣𝐵
41 nfs1v 2254 . . . . . . . . . . . . . . . . . . . 20 𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜏
42 nfs1v 2254 . . . . . . . . . . . . . . . . . . . . . 22 𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜃
43 nfv 1957 . . . . . . . . . . . . . . . . . . . . . 22 𝑣 𝑢 = 𝑤
4442, 43nfim 1943 . . . . . . . . . . . . . . . . . . . . 21 𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)
4540, 44nfral 3127 . . . . . . . . . . . . . . . . . . . 20 𝑣𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)
4641, 45nfan 1946 . . . . . . . . . . . . . . . . . . 19 𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤))
4740, 46nfrex 3188 . . . . . . . . . . . . . . . . . 18 𝑣𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤))
48 nfv 1957 . . . . . . . . . . . . . . . . . 18 𝑣 𝑥 = 𝑎
4947, 48nfim 1943 . . . . . . . . . . . . . . . . 17 𝑣(∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)
5039, 49nfan 1946 . . . . . . . . . . . . . . . 16 𝑣(∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎))
51 sbequ12 2229 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜏))
52 sbequ12 2229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜃))
5352imbi1d 333 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜃𝑢 = 𝑤) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
5453ralbidv 3168 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → (∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤) ↔ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
5551, 54anbi12d 624 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤))))
5655rexbidv 3237 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) ↔ ∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤))))
57 equequ2 2073 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (𝑥 = 𝑣𝑥 = 𝑎))
5856, 57imbi12d 336 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑎 → ((∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)))
5958anbi2d 622 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑎 → ((∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎))))
6050, 59rspc 3505 . . . . . . . . . . . . . . 15 (𝑎𝐴 → (∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎))))
6160ad2antrl 718 . . . . . . . . . . . . . 14 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → (∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎))))
62 nfs1v 2254 . . . . . . . . . . . . . . . . . . . . 21 𝑤[𝑏 / 𝑤]𝜒
63 nfv 1957 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑦 = 𝑏
6462, 63nfim 1943 . . . . . . . . . . . . . . . . . . . 20 𝑤([𝑏 / 𝑤]𝜒𝑦 = 𝑏)
65 sbequ12 2229 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑏 → (𝜒 ↔ [𝑏 / 𝑤]𝜒))
66 equequ2 2073 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑏 → (𝑦 = 𝑤𝑦 = 𝑏))
6765, 66imbi12d 336 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑏 → ((𝜒𝑦 = 𝑤) ↔ ([𝑏 / 𝑤]𝜒𝑦 = 𝑏)))
6864, 67rspc 3505 . . . . . . . . . . . . . . . . . . 19 (𝑏𝐵 → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒𝑦 = 𝑏)))
6968adantl 475 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝑏𝐵) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒𝑦 = 𝑏)))
7069adantl 475 . . . . . . . . . . . . . . . . 17 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒𝑦 = 𝑏)))
7170imp 397 . . . . . . . . . . . . . . . 16 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → ([𝑏 / 𝑤]𝜒𝑦 = 𝑏))
72 nfv 1957 . . . . . . . . . . . . . . . . . . . . . 22 𝑦𝜒
7372, 1sbiev 2286 . . . . . . . . . . . . . . . . . . . . 21 ([𝑤 / 𝑦]𝜑𝜒)
7473bicomi 216 . . . . . . . . . . . . . . . . . . . 20 (𝜒 ↔ [𝑤 / 𝑦]𝜑)
7574sbbii 2019 . . . . . . . . . . . . . . . . . . 19 ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑤][𝑤 / 𝑦]𝜑)
76 nfv 1957 . . . . . . . . . . . . . . . . . . . 20 𝑤𝜑
7776sbco2 2492 . . . . . . . . . . . . . . . . . . 19 ([𝑏 / 𝑤][𝑤 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)
7875, 77bitri 267 . . . . . . . . . . . . . . . . . 18 ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑦]𝜑)
7978imbi1i 341 . . . . . . . . . . . . . . . . 17 (([𝑏 / 𝑤]𝜒𝑦 = 𝑏) ↔ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏))
80 nfv 1957 . . . . . . . . . . . . . . . . . . . . . . 23 𝑦𝜂
81 2reu8i.b . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑏 → (𝜑𝜂))
8280, 81sbie 2484 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑏 / 𝑦]𝜑𝜂)
83 pm3.35 793 . . . . . . . . . . . . . . . . . . . . . . . 24 (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → 𝑦 = 𝑏)
8483equcomd 2066 . . . . . . . . . . . . . . . . . . . . . . 23 (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → 𝑏 = 𝑦)
8584ex 403 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑏 / 𝑦]𝜑 → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → 𝑏 = 𝑦))
8682, 85sylbir 227 . . . . . . . . . . . . . . . . . . . . 21 (𝜂 → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → 𝑏 = 𝑦))
8786com12 32 . . . . . . . . . . . . . . . . . . . 20 (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → (𝜂𝑏 = 𝑦))
8887ad2antlr 717 . . . . . . . . . . . . . . . . . . 19 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂𝑏 = 𝑦))
89 simplrr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → 𝑏𝐵)
9089ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → 𝑏𝐵)
91 nfv 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑥 𝑢 = 𝑏
92 sbequ 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → ([𝑢 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
9391, 92sbbid 2227 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
94 equequ1 2072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 = 𝑏 → (𝑢 = 𝑤𝑏 = 𝑤))
9594imbi2d 332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
9695ralbidv 3168 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → (∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤) ↔ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
9793, 96anbi12d 624 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤))))
9897adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) ∧ 𝑢 = 𝑏) → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤))))
99 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑎 ∈ V
100 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑏 ∈ V
101 2reu8i.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑𝜓))
10299, 100, 101sbc2ie 3723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜓)
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜓))
104103biimprd 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → (𝜓[𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
105104adantld 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → ((𝜂𝜓) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
106105imp 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
107 sbsbc 3656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑏 / 𝑦]𝜑[𝑏 / 𝑦]𝜑)
108107sbbii 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
109 sbsbc 3656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑[𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
110108, 109bitri 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑[𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
111106, 110sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
11272, 1sbie 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ([𝑤 / 𝑦]𝜑𝜒)
113112sbbii 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑎 / 𝑥]𝜒)
114 nfv 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑥𝜁
115 2reu8i.a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑎 → (𝜒𝜁))
116114, 115sbie 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ([𝑎 / 𝑥]𝜒𝜁)
117113, 116bitri 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝜁)
118 2reu8i.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜒𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤)
119118ex 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜒𝑦 = 𝑤) → (𝜁𝑦 = 𝑤))
120119adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) ∧ (𝜒𝑦 = 𝑤)) → (𝜁𝑦 = 𝑤))
12182imbi1i 341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) ↔ (𝜂𝑦 = 𝑏))
122 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜂 → ((𝜂𝑦 = 𝑏) → 𝑦 = 𝑏))
123122ad2antrl 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) → ((𝜂𝑦 = 𝑏) → 𝑦 = 𝑏))
124121, 123syl5bi 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → 𝑦 = 𝑏))
125 ax7 2063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑏 → (𝑦 = 𝑤𝑏 = 𝑤))
126124, 125syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → (𝑦 = 𝑤𝑏 = 𝑤)))
127126imp 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → (𝑦 = 𝑤𝑏 = 𝑤))
128127ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) ∧ (𝜒𝑦 = 𝑤)) → (𝑦 = 𝑤𝑏 = 𝑤))
129120, 128syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) ∧ (𝜒𝑦 = 𝑤)) → (𝜁𝑏 = 𝑤))
130117, 129syl5bi 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) ∧ (𝜒𝑦 = 𝑤)) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤))
131130ex 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) → ((𝜒𝑦 = 𝑤) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
132131ralimdva 3144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
133132exp31 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → ((𝜂𝜓) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))))
134133com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → ((𝜂𝜓) → ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))))
135134imp41 418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤))
136111, 135jca 507 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
13790, 98, 136rspcedvd 3518 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ∃𝑢𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)))
138 nfv 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑥𝜏
139138, 4sbiev 2286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑣 / 𝑥]𝜑𝜏)
140139bicomi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜏 ↔ [𝑣 / 𝑥]𝜑)
141140sbbii 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑢 / 𝑦]𝜏 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜑)
142 sbcom2 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑢 / 𝑦][𝑣 / 𝑥]𝜑 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
143141, 142bitri 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ([𝑢 / 𝑦]𝜏 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
144143sbbii 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
145 nfv 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑣[𝑢 / 𝑦]𝜑
146145sbco2 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
147144, 146bitri 267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
148 nfv 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑥𝜃
149148, 5sbiev 2286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ([𝑣 / 𝑥]𝜒𝜃)
150149bicomi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜃 ↔ [𝑣 / 𝑥]𝜒)
151150sbbii 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑢 / 𝑦]𝜃 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜒)
152 sbcom2 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑢 / 𝑦][𝑣 / 𝑥]𝜒 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
153151, 152bitri 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ([𝑢 / 𝑦]𝜃 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
154153sbbii 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
155 nfv 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑣[𝑢 / 𝑦]𝜒
156155sbco2 2492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜒)
15774sbbii 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑢 / 𝑦]𝜒 ↔ [𝑢 / 𝑦][𝑤 / 𝑦]𝜑)
158 nfs1v 2254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑦[𝑤 / 𝑦]𝜑
159158sbf 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑢 / 𝑦][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦]𝜑)
160157, 159bitri 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ([𝑢 / 𝑦]𝜒 ↔ [𝑤 / 𝑦]𝜑)
161160sbbii 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
162154, 156, 1613bitri 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
163162imbi1i 341 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤))
164163ralbii 3162 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤) ↔ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤))
165147, 164anbi12i 620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)))
166165rexbii 3224 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) ↔ ∃𝑢𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)))
167137, 166sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
168 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
169167, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
170169impancom 445 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → ((𝜂𝜓) → 𝑥 = 𝑎))
171170imp 397 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂𝜓)) → 𝑥 = 𝑎)
172171equcomd 2066 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂𝜓)) → 𝑎 = 𝑥)
173172exp32 413 . . . . . . . . . . . . . . . . . . 19 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝜓𝑎 = 𝑥)))
17488, 173jcad 508 . . . . . . . . . . . . . . . . . 18 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))
175174exp31 412 . . . . . . . . . . . . . . . . 17 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
17679, 175syl5bi 234 . . . . . . . . . . . . . . . 16 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → (([𝑏 / 𝑤]𝜒𝑦 = 𝑏) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
17771, 176mpd 15 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
178177expimpd 447 . . . . . . . . . . . . . 14 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → ((∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
17961, 178syld 47 . . . . . . . . . . . . 13 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → (∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
180179impancom 445 . . . . . . . . . . . 12 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ((𝑎𝐴𝑏𝐵) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
181180ralrimivv 3152 . . . . . . . . . . 11 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))
18238, 181jca 507 . . . . . . . . . 10 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
183182ex 403 . . . . . . . . 9 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
18437, 183syl5 34 . . . . . . . 8 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ((∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
185184expd 406 . . . . . . 7 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → (∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))))
186185expimpd 447 . . . . . 6 ((𝑥𝐴𝑦𝐵) → ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → (∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))))
187186impd 400 . . . . 5 ((𝑥𝐴𝑦𝐵) → (((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
188187reximdva 3198 . . . 4 (𝑥𝐴 → (∃𝑦𝐵 ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
18936, 188syl5bi 234 . . 3 (𝑥𝐴 → ((∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
190189reximia 3190 . 2 (∃𝑥𝐴 (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
19111, 190sylbi 209 1 (∃!𝑥𝐴 ∃!𝑦𝐵 𝜑 → ∃𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  [wsb 2011  wcel 2107  wral 3090  wrex 3091  ∃!wreu 3092  [wsbc 3652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-reu 3097  df-v 3400  df-sbc 3653
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator