Theorem reuxfrdf 33087

Description: Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3705 (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 3696	. . . . . . 7 ⊢ (∃*𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
3	1, 2	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
4		ancom 466	. . . . . . 7 ⊢ ((𝜓 ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ 𝜓))
5	4	rmobii 3373	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴) ↔ ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
6	3, 5	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
7	6	ralrimiva 3154	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
8		df-rmo 3365	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
9	8	ralbii 3108	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
10		df-ral 3077	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
11		reuxfrdf.0	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐵
12	11	nfcri 2914	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐵
13	12	moanim 2645	. . . . . . . 8 ⊢ (∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
14	13	albii 1851	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
15	10, 14	bitr4i 281	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
16		2euswapv 2655	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
17		df-reu 3366	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
18	12	r19.41 3266	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
19		ancom 466	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
20	19	rexbii 3109	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
21		ancom 466	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
22	18, 20, 21	3bitr4i 306	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
23		df-rex 3087	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
24	22, 23	bitr3i 280	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
25		an12 658	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
26	25	exbii 1880	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
27	24, 26	bitri 278	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
28	27	eubii 2610	. . . . . . . 8 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
29	17, 28	bitri 278	. . . . . . 7 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
30		df-reu 3366	. . . . . . . 8 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
31		nfv 1946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐶
32	31	r19.41 3266	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
33		ancom 466	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
34	33	rexbii 3109	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
35		ancom 466	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
36	32, 34, 35	3bitr4i 306	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
37		df-rex 3087	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
38	36, 37	bitr3i 280	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
39	38	eubii 2610	. . . . . . . 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 18	. . 3 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
45		df-ral 3077	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
46		moanimv 2644	. . . . . . 7 ⊢ (∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
47	46	albii 1851	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
48	45, 47	bitr4i 281	. . . . 5 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
49		2euswapv 2655	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
50		r19.42v 3194	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
51	50, 37	bitr3i 280	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
52		an12 658	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
53	52	exbii 1880	. . . . . . . . 9 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
54	51, 53	bitri 278	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
55	54	eubii 2610	. . . . . . 7 ⊢ (∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
56	30, 55	bitri 278	. . . . . 6 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
57	24	eubii 2610	. . . . . . 7 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
58	17, 57	bitri 278	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
59	49, 56, 58	3imtr4g 299	. . . . 5 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
60	48, 59	sylbi 220	. . . 4 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
61		moeq 3664	. . . . . . 7 ⊢ ∃*𝑥 𝑥 = 𝐴
62	61	moani 2578	. . . . . 6 ⊢ ∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴)
63		ancom 466	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)))
64		an12 658	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
65	63, 64	bitri 278	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
66	65	mobii 2573	. . . . . 6 ⊢ (∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
67	62, 66	mpbi 233	. . . . 5 ⊢ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))
68	67	a1i 11	. . . 4 ⊢ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
69	60, 68	mprg 3082	. . 3 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
70	44, 69	impbid1 228	. 2 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
71		reuxfrdf.1	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)
72		biidd 265	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜓))
73	72	ceqsrexv 3608	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
74	71, 73	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
75	74	reubidva 3379	. 2 ⊢ (𝜑 → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))
76	70, 75	bitrd 282	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∃*wmo 2562  ∃!weu 2593  Ⅎwnfc 2907  ∀wral 3076  ∃wrex 3086  ∃!wreu 3363  ∃*wrmo 3364

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-rmo 3365  df-reu 3366

This theorem is used by: (None)