Theorem rexeqif

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

	Ref	Expression
Hypotheses	rexeqif.1	|- F/_ x A
	rexeqif.2	|- F/_ x B
	rexeqif.3	|- A = B
Assertion	rexeqif	|- ( E. x e. A ph <-> E. x e. B ph )

Proof

Step	Hyp	Ref	Expression
1		rexeqif.1	|- F/_ x A
2		rexeqif.2	|- F/_ x B
3		rexeqif.3	|- A = B
4	1 2	rexeqf	|- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) )
5	3 4	ax-mp	|- ( E. x e. A ph <-> E. x e. B ph )