Theorem rexeqif

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

	Ref	Expression
Hypotheses	rexeqif.1	$$⊢\underset{\_}{Ⅎ}xA$$
	rexeqif.2	$$⊢\underset{\_}{Ⅎ}xB$$
	rexeqif.3	$$⊢A=B$$
Assertion	rexeqif	$$⊢\exists x\in A\phi \leftrightarrow \exists x\in B\phi$$

Proof

Step	Hyp	Ref	Expression
1		rexeqif.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		rexeqif.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		rexeqif.3	$$⊢A=B$$
4	1 2	rexeqf	$$⊢A=B\to \left(\exists x\in A\phi \leftrightarrow \exists x\in B\phi \right)$$
5	3 4	ax-mp	$$⊢\exists x\in A\phi \leftrightarrow \exists x\in B\phi$$