Theorem reuxfrdf 30255

Description: Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3739 (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 3730	. . . . . . 7 ⊢ (∃*𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
3	1, 2	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
4		ancom 463	. . . . . . 7 ⊢ ((𝜓 ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ 𝜓))
5	4	rmobii 3396	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴) ↔ ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
6	3, 5	sylib 220	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
7	6	ralrimiva 3182	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
8		df-rmo 3146	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
9	8	ralbii 3165	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
10		df-ral 3143	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
11		reuxfrdf.0	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐵
12	11	nfcri 2971	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐵
13	12	moanim 2705	. . . . . . . 8 ⊢ (∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
14	13	albii 1820	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
15	10, 14	bitr4i 280	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
16		2euswapv 2715	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
17		df-reu 3145	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
18	12	r19.41 3348	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
19		ancom 463	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
20	19	rexbii 3247	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
21		ancom 463	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
22	18, 20, 21	3bitr4i 305	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
23		df-rex 3144	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
24	22, 23	bitr3i 279	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
25		an12 643	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
26	25	exbii 1848	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
27	24, 26	bitri 277	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
28	27	eubii 2670	. . . . . . . 8 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
29	17, 28	bitri 277	. . . . . . 7 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
30		df-reu 3145	. . . . . . . 8 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
31		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐶
32	31	r19.41 3348	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
33		ancom 463	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
34	33	rexbii 3247	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
35		ancom 463	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
36	32, 34, 35	3bitr4i 305	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
37		df-rex 3144	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
38	36, 37	bitr3i 279	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
39	38	eubii 2670	. . . . . . . 8 ⊢ (∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
40	30, 39	bitri 277	. . . . . . 7 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
41	16, 29, 40	3imtr4g 298	. . . . . 6 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
42	15, 41	sylbi 219	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
43	9, 42	sylbi 219	. . . 4 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
44	7, 43	syl 17	. . 3 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
45		df-ral 3143	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
46		moanimv 2704	. . . . . . 7 ⊢ (∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
47	46	albii 1820	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
48	45, 47	bitr4i 280	. . . . 5 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
49		2euswapv 2715	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
50		r19.42v 3350	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
51	50, 37	bitr3i 279	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
52		an12 643	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
53	52	exbii 1848	. . . . . . . . 9 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
54	51, 53	bitri 277	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
55	54	eubii 2670	. . . . . . 7 ⊢ (∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
56	30, 55	bitri 277	. . . . . 6 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
57	24	eubii 2670	. . . . . . 7 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
58	17, 57	bitri 277	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
59	49, 56, 58	3imtr4g 298	. . . . 5 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
60	48, 59	sylbi 219	. . . 4 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
61		moeq 3698	. . . . . . 7 ⊢ ∃*𝑥 𝑥 = 𝐴
62	61	moani 2637	. . . . . 6 ⊢ ∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴)
63		ancom 463	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)))
64		an12 643	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
65	63, 64	bitri 277	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
66	65	mobii 2631	. . . . . 6 ⊢ (∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
67	62, 66	mpbi 232	. . . . 5 ⊢ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))
68	67	a1i 11	. . . 4 ⊢ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
69	60, 68	mprg 3152	. . 3 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
70	44, 69	impbid1 227	. 2 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
71		reuxfrdf.1	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)
72		biidd 264	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜓))
73	72	ceqsrexv 3649	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
74	71, 73	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
75	74	reubidva 3388	. 2 ⊢ (𝜑 → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))
76	70, 75	bitrd 281	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∃*wmo 2620  ∃!weu 2653  Ⅎwnfc 2961  ∀wral 3138  ∃wrex 3139  ∃!wreu 3140  ∃*wrmo 3141

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 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146

This theorem is referenced by: (None)