Theorem reuxfrdf 32952

Description: Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3709 (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 3700	. . . . . . 7 ⊢ (∃*𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
3	1, 2	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
4		ancom 466	. . . . . . 7 ⊢ ((𝜓 ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ 𝜓))
5	4	rmobii 3375	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴) ↔ ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
6	3, 5	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
7	6	ralrimiva 3156	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
8		df-rmo 3367	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
9	8	ralbii 3110	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
10		df-ral 3079	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
11		reuxfrdf.0	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐵
12	11	nfcri 2916	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐵
13	12	moanim 2647	. . . . . . . 8 ⊢ (∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
14	13	albii 1852	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
15	10, 14	bitr4i 281	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
16		2euswapv 2657	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
17		df-reu 3368	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
18	12	r19.41 3268	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
19		ancom 466	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
20	19	rexbii 3111	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
21		ancom 466	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
22	18, 20, 21	3bitr4i 306	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
23		df-rex 3089	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
24	22, 23	bitr3i 280	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
25		an12 658	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
26	25	exbii 1881	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
27	24, 26	bitri 278	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
28	27	eubii 2612	. . . . . . . 8 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
29	17, 28	bitri 278	. . . . . . 7 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
30		df-reu 3368	. . . . . . . 8 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
31		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐶
32	31	r19.41 3268	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
33		ancom 466	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
34	33	rexbii 3111	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
35		ancom 466	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
36	32, 34, 35	3bitr4i 306	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
37		df-rex 3089	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
38	36, 37	bitr3i 280	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
39	38	eubii 2612	. . . . . . . 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 3079	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
46		moanimv 2646	. . . . . . 7 ⊢ (∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
47	46	albii 1852	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
48	45, 47	bitr4i 281	. . . . 5 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
49		2euswapv 2657	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
50		r19.42v 3196	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
51	50, 37	bitr3i 280	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
52		an12 658	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
53	52	exbii 1881	. . . . . . . . 9 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
54	51, 53	bitri 278	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
55	54	eubii 2612	. . . . . . 7 ⊢ (∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
56	30, 55	bitri 278	. . . . . 6 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
57	24	eubii 2612	. . . . . . 7 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
58	17, 57	bitri 278	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
59	49, 56, 58	3imtr4g 299	. . . . 5 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
60	48, 59	sylbi 220	. . . 4 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
61		moeq 3668	. . . . . . 7 ⊢ ∃*𝑥 𝑥 = 𝐴
62	61	moani 2580	. . . . . 6 ⊢ ∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴)
63		ancom 466	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)))
64		an12 658	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
65	63, 64	bitri 278	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
66	65	mobii 2575	. . . . . 6 ⊢ (∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
67	62, 66	mpbi 233	. . . . 5 ⊢ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))
68	67	a1i 11	. . . 4 ⊢ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
69	60, 68	mprg 3084	. . 3 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
70	44, 69	impbid1 228	. 2 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
71		reuxfrdf.1	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)
72		biidd 265	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜓))
73	72	ceqsrexv 3612	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
74	71, 73	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
75	74	reubidva 3381	. 2 ⊢ (𝜑 → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))
76	70, 75	bitrd 282	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃*wmo 2564  ∃!weu 2595  Ⅎwnfc 2909  ∀wral 3078  ∃wrex 3088  ∃!wreu 3365  ∃*wrmo 3366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368

This theorem is used by: (None)