Metamath Proof Explorer

Theorem ralidmOLD

Description: Obsolete version of ralidm as of 2-Sep-2024. (Contributed by NM, 28-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ralidmOLD ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x ∈ A φ

Proof

Step Hyp Ref Expression
1 rzal ⊢ A = ∅ → ∀ x ∈ A ∀ x ∈ A φ
2 rzal ⊢ A = ∅ → ∀ x ∈ A φ
3 1 2 2thd ⊢ A = ∅ → ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x ∈ A φ
4 neq0 ⊢ ¬ A = ∅ ↔ ∃ x x ∈ A
5 df-ral ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x x ∈ A → ∀ x ∈ A φ
6 nfra1 ⊢ Ⅎ x ∀ x ∈ A φ
7 6 19.23 ⊢ ∀ x x ∈ A → ∀ x ∈ A φ ↔ ∃ x x ∈ A → ∀ x ∈ A φ
8 5 7 bitri ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∃ x x ∈ A → ∀ x ∈ A φ
9 biimt ⊢ ∃ x x ∈ A → ∀ x ∈ A φ ↔ ∃ x x ∈ A → ∀ x ∈ A φ
10 8 9 bitr4id ⊢ ∃ x x ∈ A → ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x ∈ A φ
11 4 10 sylbi ⊢ ¬ A = ∅ → ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x ∈ A φ
12 3 11 pm2.61i ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x ∈ A φ