Metamath Proof Explorer


Theorem rexeqtrdv

Description: Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025)

Ref Expression
Hypotheses rexeqtrdv.1 φ x A ψ
rexeqtrdv.2 φ A = B
Assertion rexeqtrdv φ x B ψ

Proof

Step Hyp Ref Expression
1 rexeqtrdv.1 φ x A ψ
2 rexeqtrdv.2 φ A = B
3 2 rexeqdv φ x A ψ x B ψ
4 1 3 mpbid φ x B ψ