Theorem euxfrw

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Version of euxfr 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	euxfrw.1	⊢ 𝐴 ∈ V
	euxfrw.2	⊢ ∃! 𝑦 𝑥 = 𝐴
	euxfrw.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	euxfrw	⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		euxfrw.1	⊢ 𝐴 ∈ V
2		euxfrw.2	⊢ ∃! 𝑦 𝑥 = 𝐴
3		euxfrw.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		euex	⊢ ( ∃! 𝑦 𝑥 = 𝐴 → ∃ 𝑦 𝑥 = 𝐴 )
5	2 4	ax-mp	⊢ ∃ 𝑦 𝑥 = 𝐴
6	5	biantrur	⊢ ( 𝜑 ↔ ( ∃ 𝑦 𝑥 = 𝐴 ∧ 𝜑 ) )
7		19.41v	⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ( ∃ 𝑦 𝑥 = 𝐴 ∧ 𝜑 ) )
8	3	pm5.32i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ 𝜓 ) )
9	8	exbii	⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
10	6 7 9	3bitr2i	⊢ ( 𝜑 ↔ ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
11	10	eubii	⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
12	2	eumoi	⊢ ∃* 𝑦 𝑥 = 𝐴
13	1 12	euxfr2w	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 𝜓 )
14	11 13	bitri	⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )