reuxfrdf

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

	Ref	Expression
Hypotheses	reuxfrdf.0	$⊢ \underline{Ⅎ} y B$
	reuxfrdf.1	$⊢ (φ \land y \in C) \to A \in B$
	reuxfrdf.2	$⊢ (φ \land x \in B) \to \exists^{*} y \in C x = A$
Assertion	reuxfrdf	$⊢ φ \to (\exists! x \in B \exists y \in C (x = A \land ψ) \leftrightarrow \exists! y \in C ψ)$

Proof

Step	Hyp	Ref	Expression
1		reuxfrdf.0	$⊢ \underline{Ⅎ} y B$
2		reuxfrdf.1	$⊢ (φ \land y \in C) \to A \in B$
3		reuxfrdf.2	$⊢ (φ \land x \in B) \to \exists^{*} y \in C x = A$
4		rmoan	$⊢ \exists^{} y \in C x = A \to \exists^{} y \in C (ψ \land x = A)$
5	3 4	syl	$⊢ (φ \land x \in B) \to \exists^{*} y \in C (ψ \land x = A)$
6		ancom	$⊢ (ψ \land x = A) \leftrightarrow (x = A \land ψ)$
7	6	rmobii	$⊢ \exists^{} y \in C (ψ \land x = A) \leftrightarrow \exists^{} y \in C (x = A \land ψ)$
8	5 7	sylib	$⊢ (φ \land x \in B) \to \exists^{*} y \in C (x = A \land ψ)$
9	8	ralrimiva	$⊢ φ \to \forall x \in B \exists^{*} y \in C (x = A \land ψ)$
10		df-rmo	$⊢ \exists^{} y \in C (x = A \land ψ) \leftrightarrow \exists^{} y (y \in C \land (x = A \land ψ))$
11	10	ralbii	$⊢ \forall x \in B \exists^{} y \in C (x = A \land ψ) \leftrightarrow \forall x \in B \exists^{} y (y \in C \land (x = A \land ψ))$
12		df-ral	$⊢ \forall x \in B \exists^{} y (y \in C \land (x = A \land ψ)) \leftrightarrow \forall x (x \in B \to \exists^{} y (y \in C \land (x = A \land ψ)))$
13	1	nfcri	$⊢ Ⅎ y x \in B$
14	13	moanim	$⊢ \exists^{} y (x \in B \land (y \in C \land (x = A \land ψ))) \leftrightarrow (x \in B \to \exists^{} y (y \in C \land (x = A \land ψ)))$
15	14	albii	$⊢ \forall x \exists^{} y (x \in B \land (y \in C \land (x = A \land ψ))) \leftrightarrow \forall x (x \in B \to \exists^{} y (y \in C \land (x = A \land ψ)))$
16	12 15	bitr4i	$⊢ \forall x \in B \exists^{} y (y \in C \land (x = A \land ψ)) \leftrightarrow \forall x \exists^{} y (x \in B \land (y \in C \land (x = A \land ψ)))$
17		2euswapv	$⊢ \forall x \exists^{*} y (x \in B \land (y \in C \land (x = A \land ψ))) \to (\exists! x \exists y (x \in B \land (y \in C \land (x = A \land ψ))) \to \exists! y \exists x (x \in B \land (y \in C \land (x = A \land ψ))))$
18		df-reu	$⊢ \exists! x \in B \exists y \in C (x = A \land ψ) \leftrightarrow \exists! x (x \in B \land \exists y \in C (x = A \land ψ))$
19	13	r19.41	$⊢ \exists y \in C ((x = A \land ψ) \land x \in B) \leftrightarrow (\exists y \in C (x = A \land ψ) \land x \in B)$
20		ancom	$⊢ (x \in B \land (x = A \land ψ)) \leftrightarrow ((x = A \land ψ) \land x \in B)$
21	20	rexbii	$⊢ \exists y \in C (x \in B \land (x = A \land ψ)) \leftrightarrow \exists y \in C ((x = A \land ψ) \land x \in B)$
22		ancom	$⊢ (x \in B \land \exists y \in C (x = A \land ψ)) \leftrightarrow (\exists y \in C (x = A \land ψ) \land x \in B)$
23	19 21 22	3bitr4i	$⊢ \exists y \in C (x \in B \land (x = A \land ψ)) \leftrightarrow (x \in B \land \exists y \in C (x = A \land ψ))$
24		df-rex	$⊢ \exists y \in C (x \in B \land (x = A \land ψ)) \leftrightarrow \exists y (y \in C \land (x \in B \land (x = A \land ψ)))$
25	23 24	bitr3i	$⊢ (x \in B \land \exists y \in C (x = A \land ψ)) \leftrightarrow \exists y (y \in C \land (x \in B \land (x = A \land ψ)))$
26		an12	$⊢ (y \in C \land (x \in B \land (x = A \land ψ))) \leftrightarrow (x \in B \land (y \in C \land (x = A \land ψ)))$
27	26	exbii	$⊢ \exists y (y \in C \land (x \in B \land (x = A \land ψ))) \leftrightarrow \exists y (x \in B \land (y \in C \land (x = A \land ψ)))$
28	25 27	bitri	$⊢ (x \in B \land \exists y \in C (x = A \land ψ)) \leftrightarrow \exists y (x \in B \land (y \in C \land (x = A \land ψ)))$
29	28	eubii	$⊢ \exists! x (x \in B \land \exists y \in C (x = A \land ψ)) \leftrightarrow \exists! x \exists y (x \in B \land (y \in C \land (x = A \land ψ)))$
30	18 29	bitri	$⊢ \exists! x \in B \exists y \in C (x = A \land ψ) \leftrightarrow \exists! x \exists y (x \in B \land (y \in C \land (x = A \land ψ)))$
31		df-reu	$⊢ \exists! y \in C \exists x \in B (x = A \land ψ) \leftrightarrow \exists! y (y \in C \land \exists x \in B (x = A \land ψ))$
32		nfv	$⊢ Ⅎ x y \in C$
33	32	r19.41	$⊢ \exists x \in B ((x = A \land ψ) \land y \in C) \leftrightarrow (\exists x \in B (x = A \land ψ) \land y \in C)$
34		ancom	$⊢ (y \in C \land (x = A \land ψ)) \leftrightarrow ((x = A \land ψ) \land y \in C)$
35	34	rexbii	$⊢ \exists x \in B (y \in C \land (x = A \land ψ)) \leftrightarrow \exists x \in B ((x = A \land ψ) \land y \in C)$
36		ancom	$⊢ (y \in C \land \exists x \in B (x = A \land ψ)) \leftrightarrow (\exists x \in B (x = A \land ψ) \land y \in C)$
37	33 35 36	3bitr4i	$⊢ \exists x \in B (y \in C \land (x = A \land ψ)) \leftrightarrow (y \in C \land \exists x \in B (x = A \land ψ))$
38		df-rex	$⊢ \exists x \in B (y \in C \land (x = A \land ψ)) \leftrightarrow \exists x (x \in B \land (y \in C \land (x = A \land ψ)))$
39	37 38	bitr3i	$⊢ (y \in C \land \exists x \in B (x = A \land ψ)) \leftrightarrow \exists x (x \in B \land (y \in C \land (x = A \land ψ)))$
40	39	eubii	$⊢ \exists! y (y \in C \land \exists x \in B (x = A \land ψ)) \leftrightarrow \exists! y \exists x (x \in B \land (y \in C \land (x = A \land ψ)))$
41	31 40	bitri	$⊢ \exists! y \in C \exists x \in B (x = A \land ψ) \leftrightarrow \exists! y \exists x (x \in B \land (y \in C \land (x = A \land ψ)))$
42	17 30 41	3imtr4g	$⊢ \forall x \exists^{*} y (x \in B \land (y \in C \land (x = A \land ψ))) \to (\exists! x \in B \exists y \in C (x = A \land ψ) \to \exists! y \in C \exists x \in B (x = A \land ψ))$
43	16 42	sylbi	$⊢ \forall x \in B \exists^{*} y (y \in C \land (x = A \land ψ)) \to (\exists! x \in B \exists y \in C (x = A \land ψ) \to \exists! y \in C \exists x \in B (x = A \land ψ))$
44	11 43	sylbi	$⊢ \forall x \in B \exists^{*} y \in C (x = A \land ψ) \to (\exists! x \in B \exists y \in C (x = A \land ψ) \to \exists! y \in C \exists x \in B (x = A \land ψ))$
45	9 44	syl	$⊢ φ \to (\exists! x \in B \exists y \in C (x = A \land ψ) \to \exists! y \in C \exists x \in B (x = A \land ψ))$
46		df-ral	$⊢ \forall y \in C \exists^{} x (x \in B \land (x = A \land ψ)) \leftrightarrow \forall y (y \in C \to \exists^{} x (x \in B \land (x = A \land ψ)))$
47		moanimv	$⊢ \exists^{} x (y \in C \land (x \in B \land (x = A \land ψ))) \leftrightarrow (y \in C \to \exists^{} x (x \in B \land (x = A \land ψ)))$
48	47	albii	$⊢ \forall y \exists^{} x (y \in C \land (x \in B \land (x = A \land ψ))) \leftrightarrow \forall y (y \in C \to \exists^{} x (x \in B \land (x = A \land ψ)))$
49	46 48	bitr4i	$⊢ \forall y \in C \exists^{} x (x \in B \land (x = A \land ψ)) \leftrightarrow \forall y \exists^{} x (y \in C \land (x \in B \land (x = A \land ψ)))$
50		2euswapv	$⊢ \forall y \exists^{*} x (y \in C \land (x \in B \land (x = A \land ψ))) \to (\exists! y \exists x (y \in C \land (x \in B \land (x = A \land ψ))) \to \exists! x \exists y (y \in C \land (x \in B \land (x = A \land ψ))))$
51		r19.42v	$⊢ \exists x \in B (y \in C \land (x = A \land ψ)) \leftrightarrow (y \in C \land \exists x \in B (x = A \land ψ))$
52	51 38	bitr3i	$⊢ (y \in C \land \exists x \in B (x = A \land ψ)) \leftrightarrow \exists x (x \in B \land (y \in C \land (x = A \land ψ)))$
53		an12	$⊢ (x \in B \land (y \in C \land (x = A \land ψ))) \leftrightarrow (y \in C \land (x \in B \land (x = A \land ψ)))$
54	53	exbii	$⊢ \exists x (x \in B \land (y \in C \land (x = A \land ψ))) \leftrightarrow \exists x (y \in C \land (x \in B \land (x = A \land ψ)))$
55	52 54	bitri	$⊢ (y \in C \land \exists x \in B (x = A \land ψ)) \leftrightarrow \exists x (y \in C \land (x \in B \land (x = A \land ψ)))$
56	55	eubii	$⊢ \exists! y (y \in C \land \exists x \in B (x = A \land ψ)) \leftrightarrow \exists! y \exists x (y \in C \land (x \in B \land (x = A \land ψ)))$
57	31 56	bitri	$⊢ \exists! y \in C \exists x \in B (x = A \land ψ) \leftrightarrow \exists! y \exists x (y \in C \land (x \in B \land (x = A \land ψ)))$
58	25	eubii	$⊢ \exists! x (x \in B \land \exists y \in C (x = A \land ψ)) \leftrightarrow \exists! x \exists y (y \in C \land (x \in B \land (x = A \land ψ)))$
59	18 58	bitri	$⊢ \exists! x \in B \exists y \in C (x = A \land ψ) \leftrightarrow \exists! x \exists y (y \in C \land (x \in B \land (x = A \land ψ)))$
60	50 57 59	3imtr4g	$⊢ \forall y \exists^{*} x (y \in C \land (x \in B \land (x = A \land ψ))) \to (\exists! y \in C \exists x \in B (x = A \land ψ) \to \exists! x \in B \exists y \in C (x = A \land ψ))$
61	49 60	sylbi	$⊢ \forall y \in C \exists^{*} x (x \in B \land (x = A \land ψ)) \to (\exists! y \in C \exists x \in B (x = A \land ψ) \to \exists! x \in B \exists y \in C (x = A \land ψ))$
62		moeq	$⊢ \exists^{*} x x = A$
63	62	moani	$⊢ \exists^{*} x ((x \in B \land ψ) \land x = A)$
64		ancom	$⊢ ((x \in B \land ψ) \land x = A) \leftrightarrow (x = A \land (x \in B \land ψ))$
65		an12	$⊢ (x = A \land (x \in B \land ψ)) \leftrightarrow (x \in B \land (x = A \land ψ))$
66	64 65	bitri	$⊢ ((x \in B \land ψ) \land x = A) \leftrightarrow (x \in B \land (x = A \land ψ))$
67	66	mobii	$⊢ \exists^{} x ((x \in B \land ψ) \land x = A) \leftrightarrow \exists^{} x (x \in B \land (x = A \land ψ))$
68	63 67	mpbi	$⊢ \exists^{*} x (x \in B \land (x = A \land ψ))$
69	68	a1i	$⊢ y \in C \to \exists^{*} x (x \in B \land (x = A \land ψ))$
70	61 69	mprg	$⊢ \exists! y \in C \exists x \in B (x = A \land ψ) \to \exists! x \in B \exists y \in C (x = A \land ψ)$
71	45 70	impbid1	$⊢ φ \to (\exists! x \in B \exists y \in C (x = A \land ψ) \leftrightarrow \exists! y \in C \exists x \in B (x = A \land ψ))$
72		biidd	$⊢ x = A \to (ψ \leftrightarrow ψ)$
73	72	ceqsrexv	$⊢ A \in B \to (\exists x \in B (x = A \land ψ) \leftrightarrow ψ)$
74	2 73	syl	$⊢ (φ \land y \in C) \to (\exists x \in B (x = A \land ψ) \leftrightarrow ψ)$
75	74	reubidva	$⊢ φ \to (\exists! y \in C \exists x \in B (x = A \land ψ) \leftrightarrow \exists! y \in C ψ)$
76	71 75	bitrd	$⊢ φ \to (\exists! x \in B \exists y \in C (x = A \land ψ) \leftrightarrow \exists! y \in C ψ)$

Metamath Proof Explorer

Theorem reuxfrdf

Proof