Metamath Proof Explorer


Theorem raleqOLD

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion raleqOLD ( 𝐴 = 𝐵 → ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑥𝐵 𝜑 ) )

Proof

Step Hyp Ref Expression
1 biidd ( 𝐴 = 𝐵 → ( 𝜑𝜑 ) )
2 1 raleqbi1dv ( 𝐴 = 𝐵 → ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑥𝐵 𝜑 ) )