Theorem 2reu8i 46306

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 46305. 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.

Step	Hyp	Ref	Expression
1		2reu8i.w	. . . . 5 ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜒))
2	1	reu8 3721	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)))
3	2	reubii 3377	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)))
4		2reu8i.x	. . . . . 6 ⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏))
5		2reu8i.v	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃))
6	5	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝑣 → ((𝜒 → 𝑦 = 𝑤) ↔ (𝜃 → 𝑦 = 𝑤)))
7	6	ralbidv 3169	. . . . . 6 ⊢ (𝑥 = 𝑣 → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)))
8	4, 7	anbi12d 630	. . . . 5 ⊢ (𝑥 = 𝑣 → ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))))
9	8	rexbidv 3170	. . . 4 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ ∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))))
10	9	reu8 3721	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)))
11	3, 10	bitri 275	. 2 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)))
12		nfv 1909	. . . . . . . . 9 ⊢ Ⅎ𝑢(𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))
13		nfs1v 2145	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑢 / 𝑦]𝜏
14		nfcv 2895	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐵
15		nfs1v 2145	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦[𝑢 / 𝑦]𝜃
16		nfv 1909	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑢 = 𝑤
17	15, 16	nfim 1891	. . . . . . . . . . 11 ⊢ Ⅎ𝑦([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
18	14, 17	nfralw 3300	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
19	13, 18	nfan 1894	. . . . . . . . 9 ⊢ Ⅎ𝑦([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
20		sbequ12 2235	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (𝜏 ↔ [𝑢 / 𝑦]𝜏))
21		sbequ12 2235	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝜃 ↔ [𝑢 / 𝑦]𝜃))
22		equequ1 2020	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑦 = 𝑤 ↔ 𝑢 = 𝑤))
23	21, 22	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → ((𝜃 → 𝑦 = 𝑤) ↔ ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
24	23	ralbidv 3169	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
25	20, 24	anbi12d 630	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → ((𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) ↔ ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
26	12, 19, 25	cbvrexw 3296	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
27	26	imbi1i 349	. . . . . . 7 ⊢ ((∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))
28	27	ralbii 3085	. . . . . 6 ⊢ (∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))
29	28	anbi2i 622	. . . . 5 ⊢ ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
30		nfcv 2895	. . . . . . 7 ⊢ Ⅎ𝑦𝐴
31	14, 19	nfrexw 3302	. . . . . . . 8 ⊢ Ⅎ𝑦∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
32		nfv 1909	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 = 𝑣
33	31, 32	nfim 1891	. . . . . . 7 ⊢ Ⅎ𝑦(∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)
34	30, 33	nfralw 3300	. . . . . 6 ⊢ Ⅎ𝑦∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)
35	34	r19.41 3252	. . . . 5 ⊢ (∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
36	29, 35	bitr4i 278	. . . 4 ⊢ ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ ∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
37		r19.28v 3181	. . . . . . . . 9 ⊢ ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
38		simplr 766	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → 𝜑)
39		nfv 1909	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑣∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)
40		nfcv 2895	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑣𝐵
41		nfs1v 2145	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜏
42		nfs1v 2145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜃
43		nfv 1909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑣 𝑢 = 𝑤
44	42, 43	nfim 1891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
45	40, 44	nfralw 3300	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑣∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
46	41, 45	nfan 1894	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
47	40, 46	nfrexw 3302	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑣∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
48		nfv 1909	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑣 𝑥 = 𝑎
49	47, 48	nfim 1891	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑣(∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)
50	39, 49	nfan 1894	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑣(∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))
51		sbequ12 2235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜏))
52		sbequ12 2235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜃))
53	52	imbi1d 341	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
54	53	ralbidv 3169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑎 → (∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
55	51, 54	anbi12d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
56	55	rexbidv 3170	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
57		equequ2 2021	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑥 = 𝑣 ↔ 𝑥 = 𝑎))
58	56, 57	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → ((∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)))
59	58	anbi2d 628	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
60	50, 59	rspc 3592	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝐴 → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
61	60	ad2antrl 725	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
62		nfs1v 2145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤[𝑏 / 𝑤]𝜒
63		nfv 1909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤 𝑦 = 𝑏
64	62, 63	nfim 1891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑤([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)
65		sbequ12 2235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑏 → (𝜒 ↔ [𝑏 / 𝑤]𝜒))
66		equequ2 2021	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑏 → (𝑦 = 𝑤 ↔ 𝑦 = 𝑏))
67	65, 66	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑏 → ((𝜒 → 𝑦 = 𝑤) ↔ ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
68	64, 67	rspc 3592	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
69	68	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
70	69	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
71	70	imp 406	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏))
72	1	sbievw 2087	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ([𝑤 / 𝑦]𝜑 ↔ 𝜒)
73	72	bicomi 223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 ↔ [𝑤 / 𝑦]𝜑)
74	73	sbbii 2071	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑤][𝑤 / 𝑦]𝜑)
75		sbco2vv 2092	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑏 / 𝑤][𝑤 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)
76	74, 75	bitri 275	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑦]𝜑)
77	76	imbi1i 349	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) ↔ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏))
78		2reu8i.b	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂))
79	78	sbievw 2087	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑏 / 𝑦]𝜑 ↔ 𝜂)
80		pm3.35 800	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → 𝑦 = 𝑏)
81	80	equcomd 2014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → 𝑏 = 𝑦)
82	81	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑏 / 𝑦]𝜑 → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑏 = 𝑦))
83	79, 82	sylbir 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜂 → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑏 = 𝑦))
84	83	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (𝜂 → 𝑏 = 𝑦))
85	84	ad2antlr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → 𝑏 = 𝑦))
86		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → 𝑏 ∈ 𝐵)
87	86	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → 𝑏 ∈ 𝐵)
88		sbequ 2078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → ([𝑢 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
89	88	sbbidv 2074	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
90		equequ1 2020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = 𝑏 → (𝑢 = 𝑤 ↔ 𝑏 = 𝑤))
91	90	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
92	91	ralbidv 3169	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → (∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
93	89, 92	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))))
94	93	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) ∧ 𝑢 = 𝑏) → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))))
95		vex 3470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑎 ∈ V
96		vex 3470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑏 ∈ V
97		2reu8i.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓))
98	95, 96, 97	sbc2ie 3852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜓)
99	98	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜓))
100	99	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (𝜓 → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
101	100	adantld 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → ((𝜂 ∧ 𝜓) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
102	101	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
103		sbsbc 3773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)
104	103	sbbii 2071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
105		sbsbc 3773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
106	104, 105	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
107	102, 106	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
108	72	sbbii 2071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑎 / 𝑥]𝜒)
109		2reu8i.a	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁))
110	109	sbievw 2087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑎 / 𝑥]𝜒 ↔ 𝜁)
111	108, 110	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ 𝜁)
112		2reu8i.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤)
113	112	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜒 → 𝑦 = 𝑤) → (𝜁 → 𝑦 = 𝑤))
114	113	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝜁 → 𝑦 = 𝑤))
115	79	imbi1i 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) ↔ (𝜂 → 𝑦 = 𝑏))
116		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜂 → ((𝜂 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
117	116	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → ((𝜂 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
118	115, 117	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
119		ax7 2011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑏 → (𝑦 = 𝑤 → 𝑏 = 𝑤))
120	118, 119	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (𝑦 = 𝑤 → 𝑏 = 𝑤)))
121	120	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (𝑦 = 𝑤 → 𝑏 = 𝑤))
122	121	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝑦 = 𝑤 → 𝑏 = 𝑤))
123	114, 122	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝜁 → 𝑏 = 𝑤))
124	111, 123	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))
125	124	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) → ((𝜒 → 𝑦 = 𝑤) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
126	125	ralimdva 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
127	126	exp31 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝜂 ∧ 𝜓) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))))
128	127	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → ((𝜂 ∧ 𝜓) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))))
129	128	imp41 425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))
130	107, 129	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
131	87, 94, 130	rspcedvd 3606	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
132	4	sbievw 2087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑣 / 𝑥]𝜑 ↔ 𝜏)
133	132	bicomi 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜏 ↔ [𝑣 / 𝑥]𝜑)
134	133	sbbii 2071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑢 / 𝑦]𝜏 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜑)
135		sbcom2 2153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑢 / 𝑦][𝑣 / 𝑥]𝜑 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
136	134, 135	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑢 / 𝑦]𝜏 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
137	136	sbbii 2071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
138		sbco2vv 2092	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
139	137, 138	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
140	5	sbievw 2087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑣 / 𝑥]𝜒 ↔ 𝜃)
141	140	bicomi 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜃 ↔ [𝑣 / 𝑥]𝜒)
142	141	sbbii 2071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦]𝜃 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜒)
143		sbcom2 2153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦][𝑣 / 𝑥]𝜒 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
144	142, 143	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ([𝑢 / 𝑦]𝜃 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
145	144	sbbii 2071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
146		sbco2vv 2092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜒)
147	73	sbbii 2071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦]𝜒 ↔ [𝑢 / 𝑦][𝑤 / 𝑦]𝜑)
148		nfs1v 2145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
149	148	sbf 2254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦]𝜑)
150	147, 149	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ([𝑢 / 𝑦]𝜒 ↔ [𝑤 / 𝑦]𝜑)
151	150	sbbii 2071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
152	145, 146, 151	3bitri 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
153	152	imbi1i 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))
154	153	ralbii 3085	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))
155	139, 154	anbi12i 626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
156	155	rexbii 3086	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
157	131, 156	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
158		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
160	159	impancom 451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → ((𝜂 ∧ 𝜓) → 𝑥 = 𝑎))
161	160	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂 ∧ 𝜓)) → 𝑥 = 𝑎)
162	161	equcomd 2014	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂 ∧ 𝜓)) → 𝑎 = 𝑥)
163	162	exp32 420	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝜓 → 𝑎 = 𝑥)))
164	85, 163	jcad 512	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))
165	164	exp31 419	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
166	77, 165	biimtrid 241	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
167	71, 166	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
168	167	expimpd 453	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
169	61, 168	syld 47	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
170	169	impancom 451	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
171	170	ralrimivv 3190	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))
172	38, 171	jca 511	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
173	172	ex 412	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
174	37, 173	syl5 34	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
175	174	expd 415	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → (∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))))
176	175	expimpd 453	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))))
177	176	impd 410	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
178	177	reximdva 3160	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
179	36, 178	biimtrid 241	. . 3 ⊢ (𝑥 ∈ 𝐴 → ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
180	179	reximia 3073	. 2 ⊢ (∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
181	11, 180	sylbi 216	1 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  [wsb 2059   ∈ wcel 2098  ∀wral 3053  ∃wrex 3062  ∃!wreu 3366  [wsbc 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-reu 3369  df-v 3468  df-sbc 3770

This theorem is referenced by: (None)