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

Metamath Proof Explorer

Theorem ralidm

Description: Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997) Reduce axiom usage. (Revised by GG, 2-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x x ∈ A → ∀ x ∈ A φ
2 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
3 ax-1 ⊢ ∀ x x ∈ A → φ → x ∈ A → ∀ x x ∈ A → φ
4 3 axc4i ⊢ ∀ x x ∈ A → φ → ∀ x x ∈ A → ∀ x x ∈ A → φ
5 pm2.21 ⊢ ¬ x ∈ A → x ∈ A → φ
6 sp ⊢ ∀ x x ∈ A → φ → x ∈ A → φ
7 5 6 ja ⊢ x ∈ A → ∀ x x ∈ A → φ → x ∈ A → φ
8 7 alimi ⊢ ∀ x x ∈ A → ∀ x x ∈ A → φ → ∀ x x ∈ A → φ
9 4 8 impbii ⊢ ∀ x x ∈ A → φ ↔ ∀ x x ∈ A → ∀ x x ∈ A → φ
10 2 bicomi ⊢ ∀ x x ∈ A → φ ↔ ∀ x ∈ A φ
11 10 imbi2i ⊢ x ∈ A → ∀ x x ∈ A → φ ↔ x ∈ A → ∀ x ∈ A φ
12 11 albii ⊢ ∀ x x ∈ A → ∀ x x ∈ A → φ ↔ ∀ x x ∈ A → ∀ x ∈ A φ
13 2 9 12 3bitrri ⊢ ∀ x x ∈ A → ∀ x ∈ A φ ↔ ∀ x ∈ A φ
14 1 13 bitri ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x ∈ A φ