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 43460
Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 43459. 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 3704 . . . 4 (∃!𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)))
32reubii 3378 . . 3 (∃!𝑥𝐴 ∃!𝑦𝐵 𝜑 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)))
4 2reu8i.x . . . . . 6 (𝑥 = 𝑣 → (𝜑𝜏))
5 2reu8i.v . . . . . . . 8 (𝑥 = 𝑣 → (𝜒𝜃))
65imbi1d 344 . . . . . . 7 (𝑥 = 𝑣 → ((𝜒𝑦 = 𝑤) ↔ (𝜃𝑦 = 𝑤)))
76ralbidv 3184 . . . . . 6 (𝑥 = 𝑣 → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ↔ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)))
84, 7anbi12d 632 . . . . 5 (𝑥 = 𝑣 → ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ↔ (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤))))
98rexbidv 3284 . . . 4 (𝑥 = 𝑣 → (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ↔ ∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤))))
109reu8 3704 . . 3 (∃!𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ↔ ∃𝑥𝐴 (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)))
113, 10bitri 277 . 2 (∃!𝑥𝐴 ∃!𝑦𝐵 𝜑 ↔ ∃𝑥𝐴 (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)))
12 nfv 1915 . . . . . . . . 9 𝑢(𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤))
13 nfs1v 2160 . . . . . . . . . 10 𝑦[𝑢 / 𝑦]𝜏
14 nfcv 2973 . . . . . . . . . . 11 𝑦𝐵
15 nfs1v 2160 . . . . . . . . . . . 12 𝑦[𝑢 / 𝑦]𝜃
16 nfv 1915 . . . . . . . . . . . 12 𝑦 𝑢 = 𝑤
1715, 16nfim 1897 . . . . . . . . . . 11 𝑦([𝑢 / 𝑦]𝜃𝑢 = 𝑤)
1814, 17nfralw 3212 . . . . . . . . . 10 𝑦𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)
1913, 18nfan 1900 . . . . . . . . 9 𝑦([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤))
20 sbequ12 2253 . . . . . . . . . 10 (𝑦 = 𝑢 → (𝜏 ↔ [𝑢 / 𝑦]𝜏))
21 sbequ12 2253 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝜃 ↔ [𝑢 / 𝑦]𝜃))
22 equequ1 2032 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑦 = 𝑤𝑢 = 𝑤))
2321, 22imbi12d 347 . . . . . . . . . . 11 (𝑦 = 𝑢 → ((𝜃𝑦 = 𝑤) ↔ ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
2423ralbidv 3184 . . . . . . . . . 10 (𝑦 = 𝑢 → (∀𝑤𝐵 (𝜃𝑦 = 𝑤) ↔ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
2520, 24anbi12d 632 . . . . . . . . 9 (𝑦 = 𝑢 → ((𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) ↔ ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤))))
2612, 19, 25cbvrexw 3421 . . . . . . . 8 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) ↔ ∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
2726imbi1i 352 . . . . . . 7 ((∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))
2827ralbii 3152 . . . . . 6 (∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))
2928anbi2i 624 . . . . 5 ((∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)))
30 nfcv 2973 . . . . . . 7 𝑦𝐴
3114, 19nfrex 3296 . . . . . . . 8 𝑦𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤))
32 nfv 1915 . . . . . . . 8 𝑦 𝑥 = 𝑣
3331, 32nfim 1897 . . . . . . 7 𝑦(∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)
3430, 33nfralw 3212 . . . . . 6 𝑦𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)
3534r19.41 3335 . . . . 5 (∃𝑦𝐵 ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)))
3629, 35bitr4i 280 . . . 4 ((∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ ∃𝑦𝐵 ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)))
37 r19.28v 3173 . . . . . . . . 9 ((∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)))
38 simplr 767 . . . . . . . . . . 11 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))) → 𝜑)
39 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑣𝑤𝐵 (𝜒𝑦 = 𝑤)
40 nfcv 2973 . . . . . . . . . . . . . . . . . . 19 𝑣𝐵
41 nfs1v 2160 . . . . . . . . . . . . . . . . . . . 20 𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜏
42 nfs1v 2160 . . . . . . . . . . . . . . . . . . . . . 22 𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜃
43 nfv 1915 . . . . . . . . . . . . . . . . . . . . . 22 𝑣 𝑢 = 𝑤
4442, 43nfim 1897 . . . . . . . . . . . . . . . . . . . . 21 𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)
4540, 44nfralw 3212 . . . . . . . . . . . . . . . . . . . 20 𝑣𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)
4641, 45nfan 1900 . . . . . . . . . . . . . . . . . . 19 𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤))
4740, 46nfrex 3296 . . . . . . . . . . . . . . . . . 18 𝑣𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤))
48 nfv 1915 . . . . . . . . . . . . . . . . . 18 𝑣 𝑥 = 𝑎
4947, 48nfim 1897 . . . . . . . . . . . . . . . . 17 𝑣(∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)
5039, 49nfan 1900 . . . . . . . . . . . . . . . 16 𝑣(∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎))
51 sbequ12 2253 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜏))
52 sbequ12 2253 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜃))
5352imbi1d 344 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜃𝑢 = 𝑤) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
5453ralbidv 3184 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑎 → (∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤) ↔ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
5551, 54anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤))))
5655rexbidv 3284 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) ↔ ∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤))))
57 equequ2 2033 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑎 → (𝑥 = 𝑣𝑥 = 𝑎))
5856, 57imbi12d 347 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑎 → ((∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)))
5958anbi2d 630 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑎 → ((∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎))))
6050, 59rspc 3590 . . . . . . . . . . . . . . 15 (𝑎𝐴 → (∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎))))
6160ad2antrl 726 . . . . . . . . . . . . . 14 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → (∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎))))
62 nfs1v 2160 . . . . . . . . . . . . . . . . . . . . 21 𝑤[𝑏 / 𝑤]𝜒
63 nfv 1915 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑦 = 𝑏
6462, 63nfim 1897 . . . . . . . . . . . . . . . . . . . 20 𝑤([𝑏 / 𝑤]𝜒𝑦 = 𝑏)
65 sbequ12 2253 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑏 → (𝜒 ↔ [𝑏 / 𝑤]𝜒))
66 equequ2 2033 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑏 → (𝑦 = 𝑤𝑦 = 𝑏))
6765, 66imbi12d 347 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑏 → ((𝜒𝑦 = 𝑤) ↔ ([𝑏 / 𝑤]𝜒𝑦 = 𝑏)))
6864, 67rspc 3590 . . . . . . . . . . . . . . . . . . 19 (𝑏𝐵 → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒𝑦 = 𝑏)))
6968adantl 484 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝑏𝐵) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒𝑦 = 𝑏)))
7069adantl 484 . . . . . . . . . . . . . . . . 17 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒𝑦 = 𝑏)))
7170imp 409 . . . . . . . . . . . . . . . 16 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → ([𝑏 / 𝑤]𝜒𝑦 = 𝑏))
721sbievw 2103 . . . . . . . . . . . . . . . . . . . . 21 ([𝑤 / 𝑦]𝜑𝜒)
7372bicomi 226 . . . . . . . . . . . . . . . . . . . 20 (𝜒 ↔ [𝑤 / 𝑦]𝜑)
7473sbbii 2081 . . . . . . . . . . . . . . . . . . 19 ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑤][𝑤 / 𝑦]𝜑)
75 sbco2vv 2108 . . . . . . . . . . . . . . . . . . 19 ([𝑏 / 𝑤][𝑤 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)
7674, 75bitri 277 . . . . . . . . . . . . . . . . . 18 ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑦]𝜑)
7776imbi1i 352 . . . . . . . . . . . . . . . . 17 (([𝑏 / 𝑤]𝜒𝑦 = 𝑏) ↔ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏))
78 2reu8i.b . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑏 → (𝜑𝜂))
7978sbievw 2103 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑏 / 𝑦]𝜑𝜂)
80 pm3.35 801 . . . . . . . . . . . . . . . . . . . . . . . 24 (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → 𝑦 = 𝑏)
8180equcomd 2026 . . . . . . . . . . . . . . . . . . . . . . 23 (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → 𝑏 = 𝑦)
8281ex 415 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑏 / 𝑦]𝜑 → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → 𝑏 = 𝑦))
8379, 82sylbir 237 . . . . . . . . . . . . . . . . . . . . 21 (𝜂 → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → 𝑏 = 𝑦))
8483com12 32 . . . . . . . . . . . . . . . . . . . 20 (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → (𝜂𝑏 = 𝑦))
8584ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂𝑏 = 𝑦))
86 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → 𝑏𝐵)
8786ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → 𝑏𝐵)
88 sbequ 2090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → ([𝑢 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
8988sbbidv 2084 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
90 equequ1 2032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 = 𝑏 → (𝑢 = 𝑤𝑏 = 𝑤))
9190imbi2d 343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
9291ralbidv 3184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → (∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤) ↔ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
9389, 92anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤))))
9493adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) ∧ 𝑢 = 𝑏) → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤))))
95 vex 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑎 ∈ V
96 vex 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑏 ∈ V
97 2reu8i.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑𝜓))
9895, 96, 97sbc2ie 3828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜓)
9998a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑𝜓))
10099biimprd 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → (𝜓[𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
101100adantld 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → ((𝜂𝜓) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
102101imp 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
103 sbsbc 3756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑏 / 𝑦]𝜑[𝑏 / 𝑦]𝜑)
104103sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
105 sbsbc 3756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑[𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
106104, 105bitri 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑[𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
107102, 106sylibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
10872sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑎 / 𝑥]𝜒)
109 2reu8i.a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑎 → (𝜒𝜁))
110109sbievw 2103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ([𝑎 / 𝑥]𝜒𝜁)
111108, 110bitri 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝜁)
112 2reu8i.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜒𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤)
113112ex 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜒𝑦 = 𝑤) → (𝜁𝑦 = 𝑤))
114113adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) ∧ (𝜒𝑦 = 𝑤)) → (𝜁𝑦 = 𝑤))
11579imbi1i 352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) ↔ (𝜂𝑦 = 𝑏))
116 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜂 → ((𝜂𝑦 = 𝑏) → 𝑦 = 𝑏))
117116ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) → ((𝜂𝑦 = 𝑏) → 𝑦 = 𝑏))
118115, 117syl5bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → 𝑦 = 𝑏))
119 ax7 2023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 = 𝑏 → (𝑦 = 𝑤𝑏 = 𝑤))
120118, 119syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → (𝑦 = 𝑤𝑏 = 𝑤)))
121120imp 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → (𝑦 = 𝑤𝑏 = 𝑤))
122121ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) ∧ (𝜒𝑦 = 𝑤)) → (𝑦 = 𝑤𝑏 = 𝑤))
123114, 122syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) ∧ (𝜒𝑦 = 𝑤)) → (𝜁𝑏 = 𝑤))
124111, 123syl5bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) ∧ (𝜒𝑦 = 𝑤)) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤))
125124ex 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ 𝑤𝐵) → ((𝜒𝑦 = 𝑤) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
126125ralimdva 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ (𝜂𝜓)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
127126exp31 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → ((𝜂𝜓) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))))
128127com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → ((𝜂𝜓) → ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))))
129128imp41 428 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤))
130107, 129jca 514 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑏 = 𝑤)))
13187, 94, 130rspcedvd 3605 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ∃𝑢𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)))
1324sbievw 2103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑣 / 𝑥]𝜑𝜏)
133132bicomi 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜏 ↔ [𝑣 / 𝑥]𝜑)
134133sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑢 / 𝑦]𝜏 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜑)
135 sbcom2 2168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑢 / 𝑦][𝑣 / 𝑥]𝜑 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
136134, 135bitri 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ([𝑢 / 𝑦]𝜏 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
137136sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
138 sbco2vv 2108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
139137, 138bitri 277 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
1405sbievw 2103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ([𝑣 / 𝑥]𝜒𝜃)
141140bicomi 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜃 ↔ [𝑣 / 𝑥]𝜒)
142141sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑢 / 𝑦]𝜃 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜒)
143 sbcom2 2168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑢 / 𝑦][𝑣 / 𝑥]𝜒 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
144142, 143bitri 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ([𝑢 / 𝑦]𝜃 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
145144sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
146 sbco2vv 2108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜒)
14773sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑢 / 𝑦]𝜒 ↔ [𝑢 / 𝑦][𝑤 / 𝑦]𝜑)
148 nfs1v 2160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑦[𝑤 / 𝑦]𝜑
149148sbf 2271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ([𝑢 / 𝑦][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦]𝜑)
150147, 149bitri 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ([𝑢 / 𝑦]𝜒 ↔ [𝑤 / 𝑦]𝜑)
151150sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
152145, 146, 1513bitri 299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
153152imbi1i 352 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤))
154153ralbii 3152 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤) ↔ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤))
155139, 154anbi12i 628 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)))
156155rexbii 3234 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) ↔ ∃𝑢𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑𝑢 = 𝑤)))
157131, 156sylibr 236 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)))
158 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (𝜂𝜓)) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
160159impancom 454 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → ((𝜂𝜓) → 𝑥 = 𝑎))
161160imp 409 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂𝜓)) → 𝑥 = 𝑎)
162161equcomd 2026 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂𝜓)) → 𝑎 = 𝑥)
163162exp32 423 . . . . . . . . . . . . . . . . . . 19 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝜓𝑎 = 𝑥)))
16485, 163jcad 515 . . . . . . . . . . . . . . . . . 18 (((((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑𝑦 = 𝑏)) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))
165164exp31 422 . . . . . . . . . . . . . . . . 17 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → (([𝑏 / 𝑦]𝜑𝑦 = 𝑏) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
16677, 165syl5bi 244 . . . . . . . . . . . . . . . 16 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → (([𝑏 / 𝑤]𝜒𝑦 = 𝑏) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
16771, 166mpd 15 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → ((∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
168167expimpd 456 . . . . . . . . . . . . . 14 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → ((∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
16961, 168syld 47 . . . . . . . . . . . . 13 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ (𝑎𝐴𝑏𝐵)) → (∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
170169impancom 454 . . . . . . . . . . . 12 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ((𝑎𝐴𝑏𝐵) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
171170ralrimivv 3177 . . . . . . . . . . 11 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))
17238, 171jca 514 . . . . . . . . . 10 ((((𝑥𝐴𝑦𝐵) ∧ 𝜑) ∧ ∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣))) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
173172ex 415 . . . . . . . . 9 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (∀𝑣𝐴 (∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
17437, 173syl5 34 . . . . . . . 8 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ((∀𝑤𝐵 (𝜒𝑦 = 𝑤) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
175174expd 418 . . . . . . 7 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (∀𝑤𝐵 (𝜒𝑦 = 𝑤) → (∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))))
176175expimpd 456 . . . . . 6 ((𝑥𝐴𝑦𝐵) → ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) → (∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))))
177176impd 413 . . . . 5 ((𝑥𝐴𝑦𝐵) → (((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
178177reximdva 3261 . . . 4 (𝑥𝐴 → (∃𝑦𝐵 ((𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑢𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤𝐵 ([𝑢 / 𝑦]𝜃𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
17936, 178syl5bi 244 . . 3 (𝑥𝐴 → ((∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥))))))
180179reximia 3229 . 2 (∃𝑥𝐴 (∃𝑦𝐵 (𝜑 ∧ ∀𝑤𝐵 (𝜒𝑦 = 𝑤)) ∧ ∀𝑣𝐴 (∃𝑦𝐵 (𝜏 ∧ ∀𝑤𝐵 (𝜃𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
18111, 180sylbi 219 1 (∃!𝑥𝐴 ∃!𝑦𝐵 𝜑 → ∃𝑥𝐴𝑦𝐵 (𝜑 ∧ ∀𝑎𝐴𝑏𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓𝑎 = 𝑥)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  [wsb 2069  wcel 2114  wral 3125  wrex 3126  ∃!wreu 3127  [wsbc 3752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-reu 3132  df-v 3475  df-sbc 3753
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator