Theorem rexeqi

Description: Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypothesis	raleq1i.1	⊢ 𝐴 = 𝐵
Assertion	rexeqi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		raleq1i.1	⊢ 𝐴 = 𝐵
2		rexeq	⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 ) )
3	1 2	ax-mp	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 )