This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexeqtrrdv

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

Ref Expression
Hypotheses rexeqtrrdv.1 ⊢ φ → ∃ x ∈ A ψ
rexeqtrrdv.2 ⊢ φ → B = A
Assertion rexeqtrrdv ⊢ φ → ∃ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 rexeqtrrdv.1 ⊢ φ → ∃ x ∈ A ψ
2 rexeqtrrdv.2 ⊢ φ → B = A
3 2 rexeqdv ⊢ φ → ∃ x ∈ B ψ ↔ ∃ x ∈ A ψ
4 1 3 mpbird ⊢ φ → ∃ x ∈ B ψ