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
|- ( ph -> E. x e. A ps )
rexeqtrdv.2
|- ( ph -> A = B )
Assertion rexeqtrdv
|- ( ph -> E. x e. B ps )

Proof

Step Hyp Ref Expression
1 rexeqtrdv.1
 |-  ( ph -> E. x e. A ps )
2 rexeqtrdv.2
 |-  ( ph -> A = B )
3 2 rexeqdv
 |-  ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )
4 1 3 mpbid
 |-  ( ph -> E. x e. B ps )