Theorem rexeqif

Description: Equality inference for restricted existential quantifier. (Contributed by Glauco Siliprandi, 15-Feb-2025)

	Ref	Expression
Hypotheses	rexeqif.1	⊢ Ⅎ 𝑥 𝐴
	rexeqif.2	⊢ Ⅎ 𝑥 𝐵
	rexeqif.3	⊢ 𝐴 = 𝐵
Assertion	rexeqif	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rexeqif.1	⊢ Ⅎ 𝑥 𝐴
2		rexeqif.2	⊢ Ⅎ 𝑥 𝐵
3		rexeqif.3	⊢ 𝐴 = 𝐵
4	1 2	rexeqf	⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 ) )
5	3 4	ax-mp	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 )