Theorem euxfr

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker euxfrw when possible. (Contributed by NM, 14-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	euxfr.1	⊢ 𝐴 ∈ V
	euxfr.2	⊢ ∃! 𝑦 𝑥 = 𝐴
	euxfr.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	euxfr	⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		euxfr.1	⊢ 𝐴 ∈ V
2		euxfr.2	⊢ ∃! 𝑦 𝑥 = 𝐴
3		euxfr.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	euxfr2	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 𝜓 )
14	11 13	bitri	⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )