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

Metamath Proof Explorer

Theorem ralidmw

Description: Idempotent law for restricted quantifier. Weak version of ralidm , which does not require ax-10 , ax-12 , but requires ax-8 . (Contributed by GG, 30-Sep-2024)

Ref Expression
Hypothesis ralidmw.1 ⊢ x = y → φ ↔ ψ
Assertion ralidmw ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x ∈ A φ

Proof

Step Hyp Ref Expression
1 ralidmw.1 ⊢ x = y → φ ↔ ψ
2 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
3 2 imbi2i ⊢ x ∈ A → ∀ x ∈ A φ ↔ x ∈ A → ∀ x x ∈ A → φ
4 3 albii ⊢ ∀ x x ∈ A → ∀ x ∈ A φ ↔ ∀ x x ∈ A → ∀ x x ∈ A → φ
5 pm2.21 ⊢ ¬ x ∈ A → x ∈ A → φ
6 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
7 6 1 imbi12d ⊢ x = y → x ∈ A → φ ↔ y ∈ A → ψ
8 7 spw ⊢ ∀ x x ∈ A → φ → x ∈ A → φ
9 5 8 ja ⊢ x ∈ A → ∀ x x ∈ A → φ → x ∈ A → φ
10 9 alimi ⊢ ∀ x x ∈ A → ∀ x x ∈ A → φ → ∀ x x ∈ A → φ
11 7 hba1w ⊢ ∀ x x ∈ A → φ → ∀ x ∀ x x ∈ A → φ
12 ax-1 ⊢ ∀ x x ∈ A → φ → x ∈ A → ∀ x x ∈ A → φ
13 11 12 alrimih ⊢ ∀ x x ∈ A → φ → ∀ x x ∈ A → ∀ x x ∈ A → φ
14 10 13 impbii ⊢ ∀ x x ∈ A → ∀ x x ∈ A → φ ↔ ∀ x x ∈ A → φ
15 4 14 bitri ⊢ ∀ x x ∈ A → ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
16 df-ral ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x x ∈ A → ∀ x ∈ A φ
17 15 16 2 3bitr4i ⊢ ∀ x ∈ A ∀ x ∈ A φ ↔ ∀ x ∈ A φ