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.

Step	Hyp	Ref	Expression
1		2reu8i.w	. . . . 5 ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜒))
2	1	reu8 3614	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)))
3	2	reubii 3316	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)))
4		2reu8i.x	. . . . . 6 ⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏))
5		2reu8i.v	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃))
6	5	imbi1d 333	. . . . . . 7 ⊢ (𝑥 = 𝑣 → ((𝜒 → 𝑦 = 𝑤) ↔ (𝜃 → 𝑦 = 𝑤)))
7	6	ralbidv 3168	. . . . . 6 ⊢ (𝑥 = 𝑣 → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)))
8	4, 7	anbi12d 624	. . . . 5 ⊢ (𝑥 = 𝑣 → ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))))
9	8	rexbidv 3237	. . . 4 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ ∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))))
10	9	reu8 3614	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)))
11	3, 10	bitri 267	. 2 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)))
12		nfv 1957	. . . . . . . . 9 ⊢ Ⅎ𝑢(𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))
13		nfs1v 2254	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑢 / 𝑦]𝜏
14		nfcv 2934	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐵
15		nfs1v 2254	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦[𝑢 / 𝑦]𝜃
16		nfv 1957	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑢 = 𝑤
17	15, 16	nfim 1943	. . . . . . . . . . 11 ⊢ Ⅎ𝑦([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
18	14, 17	nfral 3127	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
19	13, 18	nfan 1946	. . . . . . . . 9 ⊢ Ⅎ𝑦([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
20		sbequ12 2229	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (𝜏 ↔ [𝑢 / 𝑦]𝜏))
21		sbequ12 2229	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝜃 ↔ [𝑢 / 𝑦]𝜃))
22		equequ1 2072	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑦 = 𝑤 ↔ 𝑢 = 𝑤))
23	21, 22	imbi12d 336	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → ((𝜃 → 𝑦 = 𝑤) ↔ ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
24	23	ralbidv 3168	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → (∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
25	20, 24	anbi12d 624	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → ((𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) ↔ ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
26	12, 19, 25	cbvrex 3364	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
27	26	imbi1i 341	. . . . . . 7 ⊢ ((∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))
28	27	ralbii 3162	. . . . . 6 ⊢ (∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))
29	28	anbi2i 616	. . . . 5 ⊢ ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
30		nfcv 2934	. . . . . . 7 ⊢ Ⅎ𝑦𝐴
31	14, 19	nfrex 3188	. . . . . . . 8 ⊢ Ⅎ𝑦∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
32		nfv 1957	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 = 𝑣
33	31, 32	nfim 1943	. . . . . . 7 ⊢ Ⅎ𝑦(∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)
34	30, 33	nfral 3127	. . . . . 6 ⊢ Ⅎ𝑦∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)
35	34	r19.41 3276	. . . . 5 ⊢ (∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)))
36	29, 35	bitr4i 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 ⊢ Ⅎ𝑣 𝑢 = 𝑤
44	42, 43	nfim 1943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
45	40, 44	nfral 3127	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑣∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)
46	41, 45	nfan 1946	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
47	40, 46	nfrex 3188	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑣∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))
48		nfv 1957	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑣 𝑥 = 𝑎
49	47, 48	nfim 1943	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑣(∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)
50	39, 49	nfan 1946	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑣(∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))
51		sbequ12 2229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜏))
52		sbequ12 2229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜃))
53	52	imbi1d 333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
54	53	ralbidv 3168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑎 → (∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
55	51, 54	anbi12d 624	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
56	55	rexbidv 3237	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))))
57		equequ2 2073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑥 = 𝑣 ↔ 𝑥 = 𝑎))
58	56, 57	imbi12d 336	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → ((∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)))
59	58	anbi2d 622	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
60	50, 59	rspc 3505	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝐴 → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
61	60	ad2antrl 718	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))))
62		nfs1v 2254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤[𝑏 / 𝑤]𝜒
63		nfv 1957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑤 𝑦 = 𝑏
64	62, 63	nfim 1943	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑤([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)
65		sbequ12 2229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑏 → (𝜒 ↔ [𝑏 / 𝑤]𝜒))
66		equequ2 2073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑏 → (𝑦 = 𝑤 ↔ 𝑦 = 𝑏))
67	65, 66	imbi12d 336	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑏 → ((𝜒 → 𝑦 = 𝑤) ↔ ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
68	64, 67	rspc 3505	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
69	68	adantl 475	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
70	69	adantl 475	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)))
71	70	imp 397	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏))
72		nfv 1957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑦𝜒
73	72, 1	sbiev 2286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ([𝑤 / 𝑦]𝜑 ↔ 𝜒)
74	73	bicomi 216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 ↔ [𝑤 / 𝑦]𝜑)
75	74	sbbii 2019	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑤][𝑤 / 𝑦]𝜑)
76		nfv 1957	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑤𝜑
77	76	sbco2 2492	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑏 / 𝑤][𝑤 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)
78	75, 77	bitri 267	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑦]𝜑)
79	78	imbi1i 341	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) ↔ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏))
80		nfv 1957	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑦𝜂
81		2reu8i.b	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂))
82	80, 81	sbie 2484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑏 / 𝑦]𝜑 ↔ 𝜂)
83		pm3.35 793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → 𝑦 = 𝑏)
84	83	equcomd 2066	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → 𝑏 = 𝑦)
85	84	ex 403	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑏 / 𝑦]𝜑 → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑏 = 𝑦))
86	82, 85	sylbir 227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜂 → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑏 = 𝑦))
87	86	com12 32	. . . . . . . . . . . . . . . . . . . 20 ⊢ (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (𝜂 → 𝑏 = 𝑦))
88	87	ad2antlr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → 𝑏 = 𝑦))
89		simplrr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → 𝑏 ∈ 𝐵)
90	89	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → 𝑏 ∈ 𝐵)
91		nfv 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑥 𝑢 = 𝑏
92		sbequ 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → ([𝑢 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
93	91, 92	sbbid 2227	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
94		equequ1 2072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = 𝑏 → (𝑢 = 𝑤 ↔ 𝑏 = 𝑤))
95	94	imbi2d 332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
96	95	ralbidv 3168	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → (∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
97	93, 96	anbi12d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))))
98	97	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) ∧ 𝑢 = 𝑏) → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))))
99		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑎 ∈ V
100		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑏 ∈ V
101		2reu8i.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓))
102	99, 100, 101	sbc2ie 3723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜓)
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜓))
104	103	biimprd 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (𝜓 → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
105	104	adantld 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → ((𝜂 ∧ 𝜓) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑))
106	105	imp 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
107		sbsbc 3656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)
108	107	sbbii 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
109		sbsbc 3656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
110	108, 109	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
111	106, 110	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)
112	72, 1	sbie 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ([𝑤 / 𝑦]𝜑 ↔ 𝜒)
113	112	sbbii 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑎 / 𝑥]𝜒)
114		nfv 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑥𝜁
115		2reu8i.a	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁))
116	114, 115	sbie 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑎 / 𝑥]𝜒 ↔ 𝜁)
117	113, 116	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ 𝜁)
118		2reu8i.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤)
119	118	ex 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜒 → 𝑦 = 𝑤) → (𝜁 → 𝑦 = 𝑤))
120	119	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝜁 → 𝑦 = 𝑤))
121	82	imbi1i 341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) ↔ (𝜂 → 𝑦 = 𝑏))
122		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜂 → ((𝜂 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
123	122	ad2antrl 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → ((𝜂 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
124	121, 123	syl5bi 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑦 = 𝑏))
125		ax7 2063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑏 → (𝑦 = 𝑤 → 𝑏 = 𝑤))
126	124, 125	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (𝑦 = 𝑤 → 𝑏 = 𝑤)))
127	126	imp 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (𝑦 = 𝑤 → 𝑏 = 𝑤))
128	127	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝑦 = 𝑤 → 𝑏 = 𝑤))
129	120, 128	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝜁 → 𝑏 = 𝑤))
130	117, 129	syl5bi 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))
131	130	ex 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) → ((𝜒 → 𝑦 = 𝑤) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
132	131	ralimdva 3144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
133	132	exp31 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝜂 ∧ 𝜓) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))))
134	133	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → ((𝜂 ∧ 𝜓) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))))
135	134	imp41 418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))
136	111, 135	jca 507	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))
137	90, 98, 136	rspcedvd 3518	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
138		nfv 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ Ⅎ𝑥𝜏
139	138, 4	sbiev 2286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑣 / 𝑥]𝜑 ↔ 𝜏)
140	139	bicomi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜏 ↔ [𝑣 / 𝑥]𝜑)
141	140	sbbii 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑢 / 𝑦]𝜏 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜑)
142		sbcom2 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑢 / 𝑦][𝑣 / 𝑥]𝜑 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
143	141, 142	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑢 / 𝑦]𝜏 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
144	143	sbbii 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑)
145		nfv 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑣[𝑢 / 𝑦]𝜑
146	145	sbco2 2492	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
147	144, 146	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑)
148		nfv 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ Ⅎ𝑥𝜃
149	148, 5	sbiev 2286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ([𝑣 / 𝑥]𝜒 ↔ 𝜃)
150	149	bicomi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜃 ↔ [𝑣 / 𝑥]𝜒)
151	150	sbbii 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦]𝜃 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜒)
152		sbcom2 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦][𝑣 / 𝑥]𝜒 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
153	151, 152	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ([𝑢 / 𝑦]𝜃 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
154	153	sbbii 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒)
155		nfv 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Ⅎ𝑣[𝑢 / 𝑦]𝜒
156	155	sbco2 2492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜒)
157	74	sbbii 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦]𝜒 ↔ [𝑢 / 𝑦][𝑤 / 𝑦]𝜑)
158		nfs1v 2254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
159	158	sbf 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ([𝑢 / 𝑦][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦]𝜑)
160	157, 159	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ([𝑢 / 𝑦]𝜒 ↔ [𝑤 / 𝑦]𝜑)
161	160	sbbii 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
162	154, 156, 161	3bitri 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑)
163	162	imbi1i 341	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))
164	163	ralbii 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))
165	147, 164	anbi12i 620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
166	165	rexbii 3224	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)))
167	137, 166	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))
168		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
169	167, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎))
170	169	impancom 445	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → ((𝜂 ∧ 𝜓) → 𝑥 = 𝑎))
171	170	imp 397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂 ∧ 𝜓)) → 𝑥 = 𝑎)
172	171	equcomd 2066	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂 ∧ 𝜓)) → 𝑎 = 𝑥)
173	172	exp32 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝜓 → 𝑎 = 𝑥)))
174	88, 173	jcad 508	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))
175	174	exp31 412	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
176	79, 175	syl5bi 234	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
177	71, 176	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
178	177	expimpd 447	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
179	61, 178	syld 47	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
180	179	impancom 445	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
181	180	ralrimivv 3152	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))
182	38, 181	jca 507	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
183	182	ex 403	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
184	37, 183	syl5 34	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
185	184	expd 406	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → (∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))))
186	185	expimpd 447	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))))
187	186	impd 400	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
188	187	reximdva 3198	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
189	36, 188	syl5bi 234	. . 3 ⊢ (𝑥 ∈ 𝐴 → ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))
190	189	reximia 3190	. 2 ⊢ (∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))
191	11, 190	sylbi 209	1 ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))

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)