Theorem 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) (Revised by Gino Giotto, 10-Jan-2024)

	Ref	Expression
Hypotheses	euxfr2w.1	⊢ 𝐴 ∈ V
	euxfr2w.2	⊢ ∃* 𝑦 𝑥 = 𝐴
Assertion	euxfr2w	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		euxfr2w.1	⊢ 𝐴 ∈ V
2		euxfr2w.2	⊢ ∃* 𝑦 𝑥 = 𝐴
3		2euswapv	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
4	2	moani	⊢ ∃* 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 )
5		ancom	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 = 𝐴 ∧ 𝜑 ) )
6	5	mobii	⊢ ( ∃* 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) ↔ ∃* 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
7	4 6	mpbi	⊢ ∃* 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 )
8	3 7	mpg	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
9		2euswapv	⊢ ( ∀ 𝑦 ∃* 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ( ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
10		moeq	⊢ ∃* 𝑥 𝑥 = 𝐴
11	10	moani	⊢ ∃* 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 )
12	5	mobii	⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) ↔ ∃* 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
13	11 12	mpbi	⊢ ∃* 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 )
14	9 13	mpg	⊢ ( ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
15	8 14	impbii	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
16		biidd	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜑 ) )
17	1 16	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜑 )
18	17	eubii	⊢ ( ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 𝜑 )
19	15 18	bitri	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 𝜑 )