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

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 ⊢ A = B → ∀ x ∈ A φ ↔ ∀ x ∈ B φ

Proof

Step Hyp Ref Expression
1 rexeq ⊢ A = B → ∃ x ∈ A ¬ φ ↔ ∃ x ∈ B ¬ φ
2 rexnal ⊢ ∃ x ∈ A ¬ φ ↔ ¬ ∀ x ∈ A φ
3 rexnal ⊢ ∃ x ∈ B ¬ φ ↔ ¬ ∀ x ∈ B φ
4 1 2 3 3bitr3g ⊢ A = B → ¬ ∀ x ∈ A φ ↔ ¬ ∀ x ∈ B φ
5 4 con4bid ⊢ A = B → ∀ x ∈ A φ ↔ ∀ x ∈ B φ