Theorem 2reu8i 48183

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 48182. 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 3690	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)))
3	2	reubii 3374	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)))
4		2reu8i.x	. . . . . 6 ⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏))
5		2reu8i.v	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃))
6	5	imbi1d 344	. . . . . . 7 ⊢ (𝑥 = 𝑣 → ((𝜒 → 𝑦 = 𝑤) ↔ (𝜃 → 𝑦 = 𝑤)))
7	6	ralbidv 3185	. . . . . 6 ⊢ (𝑥 = 𝑣 → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)))
8	4, 7	anbi12d 644	. . . . 5 ⊢ (𝑥 = 𝑣 → ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))))
9	8	rexbidv 3186	. . . 4 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ ∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))))
10	9	reu8 3690	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)))
11	3, 10	bitri 278	. 2 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)))
12		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑢(𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))
13		nfs1v 2192	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑢 / 𝑦]𝜏
14		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐵
15		nfs1v 2192	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦[𝑢 / 𝑦]𝜃
16		nfv 1946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑢 = 𝑤
17	15, 16	nfim 1928	. . . . . . . . . . 11 ⊢ Ⅎ𝑦([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
18	14, 17	nfralw 3309	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
19	13, 18	nfan 1931	. . . . . . . . 9 ⊢ Ⅎ𝑦([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
20		sbequ12 2286	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (𝜏 ↔ [𝑢 / 𝑦]𝜏))
21		sbequ12 2286	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝜃 ↔ [𝑢 / 𝑦]𝜃))
22		equequ1 2057	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑦 = 𝑤 ↔ 𝑢 = 𝑤))
23	21, 22	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → ((𝜃 → 𝑦 = 𝑤) ↔ ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
24	23	ralbidv 3185	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
25	20, 24	anbi12d 644	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → ((𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) ↔ ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
26	12, 19, 25	cbvrexw 3305	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
27	26	imbi1i 352	. . . . . . 7 ⊢ ((∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))
28	27	ralbii 3108	. . . . . 6 ⊢ (∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))
29	28	anbi2i 635	. . . . 5 ⊢ ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
30		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑦𝐴
31	14, 19	nfrexw 3310	. . . . . . . 8 ⊢ Ⅎ𝑦∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
32		nfv 1946	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 = 𝑣
33	31, 32	nfim 1928	. . . . . . 7 ⊢ Ⅎ𝑦(∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)
34	30, 33	nfralw 3309	. . . . . 6 ⊢ Ⅎ𝑦∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)
35	34	r19.41 3266	. . . . 5 ⊢ (∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
36	29, 35	bitr4i 281	. . . 4 ⊢ ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ ∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
37		r19.28v 3193	. . . . . . . . 9 ⊢ ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
38		simplr 781	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → 𝜑)
39		nfv 1946	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑣∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)
40		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑣𝐵
41		nfs1v 2192	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜏
42		nfs1v 2192	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜃
43		nfv 1946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑣 𝑢 = 𝑤
44	42, 43	nfim 1928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
45	40, 44	nfralw 3309	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑣∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
46	41, 45	nfan 1931	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
47	40, 46	nfrexw 3310	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑣∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
48		nfv 1946	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑣 𝑥 = 𝑎
49	47, 48	nfim 1928	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑣(∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)
50	39, 49	nfan 1931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑣(∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))
51		sbequ12 2286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜏))
52		sbequ12 2286	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜃))
53	52	imbi1d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
54	53	ralbidv 3185	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑎 → (∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
55	51, 54	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
56	55	rexbidv 3186	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
57		equequ2 2058	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑥 = 𝑣 ↔ 𝑥 = 𝑎))
58	56, 57	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → ((∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)))
59	58	anbi2d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
60	50, 59	rspc 3564	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝐴 → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
61	60	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
62		nfs1v 2192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤[𝑏 / 𝑤]𝜒
63		nfv 1946	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤 𝑦 = 𝑏
64	62, 63	nfim 1928	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑤([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)
65		sbequ12 2286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑏 → (𝜒 ↔ [𝑏 / 𝑤]𝜒))
66		equequ2 2058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑏 → (𝑦 = 𝑤 ↔ 𝑦 = 𝑏))
67	65, 66	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑏 → ((𝜒 → 𝑦 = 𝑤) ↔ ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
68	64, 67	rspc 3564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
69	68	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
70	69	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
71	70	imp 412	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏))
72	1	sbievw 2130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ([𝑤 / 𝑦]𝜑 ↔ 𝜒)
73	72	bicomi 227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 ↔ [𝑤 / 𝑦]𝜑)
74	73	sbbii 2112	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑤][𝑤 / 𝑦]𝜑)
75		sbco2vv 2135	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑏 / 𝑤][𝑤 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)
76	74, 75	bitri 278	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑦]𝜑)
77	76	imbi1i 352	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) ↔ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏))
78		2reu8i.b	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂))
79	78	sbievw 2130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑏 / 𝑦]𝜑 ↔ 𝜂)
80		pm3.35 815	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → 𝑦 = 𝑏)
81	80	equcomd 2051	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → 𝑏 = 𝑦)
82	81	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑏 / 𝑦]𝜑 → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑏 = 𝑦))
83	79, 82	sylbir 238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜂 → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑏 = 𝑦))
84	83	com12 33	. . . . . . . . . . . . . . . . . . . 20 ⊢ (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (𝜂 → 𝑏 = 𝑦))
85	84	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → 𝑏 = 𝑦))
86		simplrr 790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → 𝑏 ∈ 𝐵)
87	86	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → 𝑏 ∈ 𝐵)
88		sbequ 2119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → ([𝑢 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
89	88	sbbidv 2115	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
90		equequ1 2057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = 𝑏 → (𝑢 = 𝑤 ↔ 𝑏 = 𝑤))
91	90	imbi2d 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
92	91	ralbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → (∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
93	89, 92	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))))
94	93	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) ∧ 𝑢 = 𝑏) → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))))
95		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑎 ∈ V
96		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑏 ∈ V
97		2reu8i.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓))
98	95, 96, 97	sbc2ie 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜓)
99	98	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜓))
100	99	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (𝜓 → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
101	100	adantld 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → ((𝜂 ∧ 𝜓) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
102	101	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
103		sbsbc 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)
104	103	sbbii 2112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
105		sbsbc 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
106	104, 105	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
107	102, 106	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
108	72	sbbii 2112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑎 / 𝑥]𝜒)
109		2reu8i.a	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁))
110	109	sbievw 2130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑎 / 𝑥]𝜒 ↔ 𝜁)
111	108, 110	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ 𝜁)
112		2reu8i.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤)
113	112	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜒 → 𝑦 = 𝑤) → (𝜁 → 𝑦 = 𝑤))
114	113	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝜁 → 𝑦 = 𝑤))
115	79	imbi1i 352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) ↔ (𝜂 → 𝑦 = 𝑏))
116		pm2.27 43	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜂 → ((𝜂 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
117	116	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → ((𝜂 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
118	115, 117	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
119		ax7 2048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑏 → (𝑦 = 𝑤 → 𝑏 = 𝑤))
120	118, 119	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (𝑦 = 𝑤 → 𝑏 = 𝑤)))
121	120	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (𝑦 = 𝑤 → 𝑏 = 𝑤))
122	121	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝑦 = 𝑤 → 𝑏 = 𝑤))
123	114, 122	syld 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝜁 → 𝑏 = 𝑤))
124	111, 123	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))
125	124	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) → ((𝜒 → 𝑦 = 𝑤) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
126	125	ralimdva 3174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
127	126	exp31 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝜂 ∧ 𝜓) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))))
128	127	com24 96	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → ((𝜂 ∧ 𝜓) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))))
129	128	imp41 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))
130	107, 129	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
131	87, 94, 130	rspcedvd 3578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
132	4	sbievw 2130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑣 / 𝑥]𝜑 ↔ 𝜏)
133	132	bicomi 227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜏 ↔ [𝑣 / 𝑥]𝜑)
134	133	sbbii 2112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑢 / 𝑦]𝜏 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜑)
135		sbcom2 2208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑢 / 𝑦][𝑣 / 𝑥]𝜑 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
136	134, 135	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑢 / 𝑦]𝜏 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
137	136	sbbii 2112	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
138		sbco2vv 2135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
139	137, 138	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
140	5	sbievw 2130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑣 / 𝑥]𝜒 ↔ 𝜃)
141	140	bicomi 227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜃 ↔ [𝑣 / 𝑥]𝜒)
142	141	sbbii 2112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦]𝜃 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜒)
143		sbcom2 2208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦][𝑣 / 𝑥]𝜒 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
144	142, 143	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ([𝑢 / 𝑦]𝜃 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
145	144	sbbii 2112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
146		sbco2vv 2135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜒)
147	73	sbbii 2112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦]𝜒 ↔ [𝑢 / 𝑦][𝑤 / 𝑦]𝜑)
148		nfs1v 2192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
149	148	sbf 2304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦]𝜑)
150	147, 149	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ([𝑢 / 𝑦]𝜒 ↔ [𝑤 / 𝑦]𝜑)
151	150	sbbii 2112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
152	145, 146, 151	3bitri 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
153	152	imbi1i 352	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))
154	153	ralbii 3108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))
155	139, 154	anbi12i 640	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
156	155	rexbii 3109	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
157	131, 156	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
158		pm2.27 43	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
159	157, 158	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
160	159	impancom 457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → ((𝜂 ∧ 𝜓) → 𝑥 = 𝑎))
161	160	imp 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂 ∧ 𝜓)) → 𝑥 = 𝑎)
162	161	equcomd 2051	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂 ∧ 𝜓)) → 𝑎 = 𝑥)
163	162	exp32 426	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝜓 → 𝑎 = 𝑥)))
164	85, 163	jcad 522	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))
165	164	exp31 425	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
166	77, 165	biimtrid 245	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
167	71, 166	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
168	167	expimpd 459	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
169	61, 168	syld 48	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
170	169	impancom 457	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
171	170	ralrimivv 3203	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))
172	38, 171	jca 521	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
173	172	ex 418	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
174	37, 173	syl5 35	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
175	174	expd 421	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → (∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))))
176	175	expimpd 459	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))))
177	176	impd 416	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
178	177	reximdva 3175	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
179	36, 178	biimtrid 245	. . 3 ⊢ (𝑥 ∈ 𝐴 → ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
180	179	reximia 3097	. 2 ⊢ (∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
181	11, 180	sylbi 220	1 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  [wsb 2098   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  ∃!wreu 3363  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-reu 3366  df-v 3452  df-sbc 3739

This theorem is used by: (None)