Theorem reuxfrdf 32472

Description: Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3731 (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 3722	. . . . . . 7 ⊢ (∃*𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
3	1, 2	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴))
4		ancom 460	. . . . . . 7 ⊢ ((𝜓 ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ 𝜓))
5	4	rmobii 3367	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝜓 ∧ 𝑥 = 𝐴) ↔ ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
6	3, 5	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
7	6	ralrimiva 3132	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
8		df-rmo 3359	. . . . . 6 ⊢ (∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
9	8	ralbii 3082	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
10		df-ral 3052	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
11		reuxfrdf.0	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐵
12	11	nfcri 2890	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐵
13	12	moanim 2619	. . . . . . . 8 ⊢ (∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
14	13	albii 1819	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
15	10, 14	bitr4i 278	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
16		2euswapv 2629	. . . . . . 7 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
17		df-reu 3360	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
18	12	r19.41 3246	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
19		ancom 460	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
20	19	rexbii 3083	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦 ∈ 𝐶 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
21		ancom 460	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑥 ∈ 𝐵))
22	18, 20, 21	3bitr4i 303	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
23		df-rex 3061	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐶 (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
24	22, 23	bitr3i 277	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
25		an12 645	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
26	25	exbii 1848	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
27	24, 26	bitri 275	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
28	27	eubii 2584	. . . . . . . 8 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
29	17, 28	bitri 275	. . . . . . 7 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
30		df-reu 3360	. . . . . . . 8 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
31		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐶
32	31	r19.41 3246	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
33		ancom 460	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
34	33	rexbii 3083	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥 ∈ 𝐵 ((𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
35		ancom 460	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ∧ 𝑦 ∈ 𝐶))
36	32, 34, 35	3bitr4i 303	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
37		df-rex 3061	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
38	36, 37	bitr3i 277	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
39	38	eubii 2584	. . . . . . . 8 ⊢ (∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
40	30, 39	bitri 275	. . . . . . 7 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
41	16, 29, 40	3imtr4g 296	. . . . . 6 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
42	15, 41	sylbi 217	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
43	9, 42	sylbi 217	. . . 4 ⊢ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
44	7, 43	syl 17	. . 3 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
45		df-ral 3052	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
46		moanimv 2618	. . . . . . 7 ⊢ (∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
47	46	albii 1819	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
48	45, 47	bitr4i 278	. . . . 5 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
49		2euswapv 2629	. . . . . 6 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))))
50		r19.42v 3176	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
51	50, 37	bitr3i 277	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
52		an12 645	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
53	52	exbii 1848	. . . . . . . . 9 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑦 ∈ 𝐶 ∧ (𝑥 = 𝐴 ∧ 𝜓))) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
54	51, 53	bitri 275	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
55	54	eubii 2584	. . . . . . 7 ⊢ (∃!𝑦(𝑦 ∈ 𝐶 ∧ ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
56	30, 55	bitri 275	. . . . . 6 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦∃𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
57	24	eubii 2584	. . . . . . 7 ⊢ (∃!𝑥(𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
58	17, 57	bitri 275	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑥∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))))
59	49, 56, 58	3imtr4g 296	. . . . 5 ⊢ (∀𝑦∃*𝑥(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
60	48, 59	sylbi 217	. . . 4 ⊢ (∀𝑦 ∈ 𝐶 ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)) → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓)))
61		moeq 3690	. . . . . . 7 ⊢ ∃*𝑥 𝑥 = 𝐴
62	61	moani 2552	. . . . . 6 ⊢ ∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴)
63		ancom 460	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)))
64		an12 645	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
65	63, 64	bitri 275	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
66	65	mobii 2547	. . . . . 6 ⊢ (∃*𝑥((𝑥 ∈ 𝐵 ∧ 𝜓) ∧ 𝑥 = 𝐴) ↔ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
67	62, 66	mpbi 230	. . . . 5 ⊢ ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓))
68	67	a1i 11	. . . 4 ⊢ (𝑦 ∈ 𝐶 → ∃*𝑥(𝑥 ∈ 𝐵 ∧ (𝑥 = 𝐴 ∧ 𝜓)))
69	60, 68	mprg 3057	. . 3 ⊢ (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) → ∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓))
70	44, 69	impbid1 225	. 2 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓)))
71		reuxfrdf.1	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)
72		biidd 262	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜓))
73	72	ceqsrexv 3634	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
74	71, 73	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ 𝜓))
75	74	reubidva 3375	. 2 ⊢ (𝜑 → (∃!𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))
76	70, 75	bitrd 279	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∃*wmo 2537  ∃!weu 2567  Ⅎwnfc 2883  ∀wral 3051  ∃wrex 3060  ∃!wreu 3357  ∃*wrmo 3358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360

This theorem is referenced by: (None)