Metamath Proof Explorer


Theorem raleq

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) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 rexeq ( 𝐴 = 𝐵 → ( ∃ 𝑥𝐴 ¬ 𝜑 ↔ ∃ 𝑥𝐵 ¬ 𝜑 ) )
2 rexnal ( ∃ 𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀ 𝑥𝐴 𝜑 )
3 rexnal ( ∃ 𝑥𝐵 ¬ 𝜑 ↔ ¬ ∀ 𝑥𝐵 𝜑 )
4 1 2 3 3bitr3g ( 𝐴 = 𝐵 → ( ¬ ∀ 𝑥𝐴 𝜑 ↔ ¬ ∀ 𝑥𝐵 𝜑 ) )
5 4 con4bid ( 𝐴 = 𝐵 → ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑥𝐵 𝜑 ) )