Metamath Proof Explorer


Theorem rexeqbi1dv

Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997) (Proof shortened by Steven Nguyen, 5-May-2023)

Ref Expression
Hypothesis raleqbi1dv.1 ( 𝐴 = 𝐵 → ( 𝜑𝜓 ) )
Assertion rexeqbi1dv ( 𝐴 = 𝐵 → ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 raleqbi1dv.1 ( 𝐴 = 𝐵 → ( 𝜑𝜓 ) )
2 id ( 𝐴 = 𝐵𝐴 = 𝐵 )
3 2 1 rexeqbidvv ( 𝐴 = 𝐵 → ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐵 𝜓 ) )