Theorem reuxfr1ds

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Use reuhypd to eliminate the second hypothesis. (Contributed by NM, 16-Jan-2012)

	Ref	Expression
Hypotheses	reuxfr1ds.1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
	reuxfr1ds.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
	reuxfr1ds.3	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
Assertion	reuxfr1ds	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		reuxfr1ds.1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
2		reuxfr1ds.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
3		reuxfr1ds.3	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
4	3	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
5	1 2 4	reuxfr1d	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )