Metamath Proof Explorer


Theorem raleqbi1dv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995) (Proof shortened by Steven Nguyen, 5-May-2023)

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

Proof

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