euxfr2w

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Version of euxfr2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 14-Nov-2004) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

	Ref	Expression
Hypotheses	euxfr2w.1	$⊢ A \in V$
	euxfr2w.2	$⊢ \exists^{*} y x = A$
Assertion	euxfr2w	$⊢ \exists! x \exists y (x = A \land φ) \leftrightarrow \exists! y φ$

Proof

Step	Hyp	Ref	Expression
1		euxfr2w.1	$⊢ A \in V$
2		euxfr2w.2	$⊢ \exists^{*} y x = A$
3		2euswapv	$⊢ \forall x \exists^{*} y (x = A \land φ) \to (\exists! x \exists y (x = A \land φ) \to \exists! y \exists x (x = A \land φ))$
4	2	moani	$⊢ \exists^{*} y (φ \land x = A)$
5		ancom	$⊢ (φ \land x = A) \leftrightarrow (x = A \land φ)$
6	5	mobii	$⊢ \exists^{} y (φ \land x = A) \leftrightarrow \exists^{} y (x = A \land φ)$
7	4 6	mpbi	$⊢ \exists^{*} y (x = A \land φ)$
8	3 7	mpg	$⊢ \exists! x \exists y (x = A \land φ) \to \exists! y \exists x (x = A \land φ)$
9		2euswapv	$⊢ \forall y \exists^{*} x (x = A \land φ) \to (\exists! y \exists x (x = A \land φ) \to \exists! x \exists y (x = A \land φ))$
10		moeq	$⊢ \exists^{*} x x = A$
11	10	moani	$⊢ \exists^{*} x (φ \land x = A)$
12	5	mobii	$⊢ \exists^{} x (φ \land x = A) \leftrightarrow \exists^{} x (x = A \land φ)$
13	11 12	mpbi	$⊢ \exists^{*} x (x = A \land φ)$
14	9 13	mpg	$⊢ \exists! y \exists x (x = A \land φ) \to \exists! x \exists y (x = A \land φ)$
15	8 14	impbii	$⊢ \exists! x \exists y (x = A \land φ) \leftrightarrow \exists! y \exists x (x = A \land φ)$
16		biidd	$⊢ x = A \to (φ \leftrightarrow φ)$
17	1 16	ceqsexv	$⊢ \exists x (x = A \land φ) \leftrightarrow φ$
18	17	eubii	$⊢ \exists! y \exists x (x = A \land φ) \leftrightarrow \exists! y φ$
19	15 18	bitri	$⊢ \exists! x \exists y (x = A \land φ) \leftrightarrow \exists! y φ$

Metamath Proof Explorer

Theorem euxfr2w

Proof