Theorem reuxfrdf 30262

Description: Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3687 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) (Revised by Thierry Arnoux, 30-Mar-2018.)

Hypotheses

Ref	Expression
reuxfrdf.0	⊢ Ⅎ𝑦𝐵
reuxfrdf.1	⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)
reuxfrdf.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 𝑥 = 𝐴)

Assertion

Ref	Expression
reuxfrdf	⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶,𝑦

Allowed substitution hints:   𝜓(𝑦)   𝐴(𝑦)   𝐵(𝑦)

Proof of Theorem reuxfrdf

Step	Hyp	Ref	Expression
1		reuxfrdf.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 𝑥 = 𝐴)
2		rmoan 3678	. . . . . . 7 ⊢ (∃*𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
3	1, 2	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
4		ancom 464	. . . . . . 7 ⊢ ((𝜓 ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ 𝜓))
5	4	rmobii 3349	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴) ↔ ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
6	3, 5	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
7	6	ralrimiva 3149	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
8		df-rmo 3114	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
9	8	ralbii 3133	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
10		df-ral 3111	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
11		reuxfrdf.0	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐵
12	11	nfcri 2943	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐵
13	12	moanim 2682	. . . . . . . 8 ⊢ (∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
14	13	albii 1821	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
15	10, 14	bitr4i 281	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
16		2euswapv 2692	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
17		df-reu 3113	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
18	12	r19.41 3301	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
19		ancom 464	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
20	19	rexbii 3210	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
21		ancom 464	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
22	18, 20, 21	3bitr4i 306	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
23		df-rex 3112	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
24	22, 23	bitr3i 280	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
25		an12 644	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
26	25	exbii 1849	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
27	24, 26	bitri 278	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
28	27	eubii 2645	. . . . . . . 8 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
29	17, 28	bitri 278	. . . . . . 7 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
30		df-reu 3113	. . . . . . . 8 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
31		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐶
32	31	r19.41 3301	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
33		ancom 464	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
34	33	rexbii 3210	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
35		ancom 464	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
36	32, 34, 35	3bitr4i 306	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
37		df-rex 3112	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
38	36, 37	bitr3i 280	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
39	38	eubii 2645	. . . . . . . 8 ⊢ (∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
40	30, 39	bitri 278	. . . . . . 7 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
41	16, 29, 40	3imtr4g 299	. . . . . 6 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
42	15, 41	sylbi 220	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
43	9, 42	sylbi 220	. . . 4 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
44	7, 43	syl 17	. . 3 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
45		df-ral 3111	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
46		moanimv 2681	. . . . . . 7 ⊢ (∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
47	46	albii 1821	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
48	45, 47	bitr4i 281	. . . . 5 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
49		2euswapv 2692	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
50		r19.42v 3303	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
51	50, 37	bitr3i 280	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
52		an12 644	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
53	52	exbii 1849	. . . . . . . . 9 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
54	51, 53	bitri 278	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
55	54	eubii 2645	. . . . . . 7 ⊢ (∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
56	30, 55	bitri 278	. . . . . 6 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
57	24	eubii 2645	. . . . . . 7 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
58	17, 57	bitri 278	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
59	49, 56, 58	3imtr4g 299	. . . . 5 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
60	48, 59	sylbi 220	. . . 4 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
61		moeq 3646	. . . . . . 7 ⊢ ∃*𝑥 𝑥 = 𝐴
62	61	moani 2612	. . . . . 6 ⊢ ∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴)
63		ancom 464	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)))
64		an12 644	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
65	63, 64	bitri 278	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
66	65	mobii 2606	. . . . . 6 ⊢ (∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
67	62, 66	mpbi 233	. . . . 5 ⊢ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))
68	67	a1i 11	. . . 4 ⊢ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
69	60, 68	mprg 3120	. . 3 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
70	44, 69	impbid1 228	. 2 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
71		reuxfrdf.1	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)
72		biidd 265	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜓))
73	72	ceqsrexv 3597	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
74	71, 73	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
75	74	reubidva 3341	. 2 ⊢ (𝜑 → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))
76	70, 75	bitrd 282	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃*wmo 2596  ∃!weu 2628  Ⅎwnfc 2936  ∀wral 3106  ∃wrex 3107  ∃!wreu 3108  ∃*wrmo 3109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114

This theorem is referenced by: (None)