Metamath Proof Explorer

Theorem wl-dfralf

Description: Restricted universal quantification ( df-wl-ral ) allows a simplification, if we can assume all appearences of x in A are bounded. (Contributed by Wolf Lammen, 23-May-2023)

Ref Expression
Assertion wl-dfralf ⊢ Ⅎ _ x A → ∀ x : A φ ↔ ∀ x x ∈ A → φ

Proof

Step Hyp Ref Expression
1 nfcr ⊢ Ⅎ _ x A → Ⅎ x y ∈ A
2 19.21t ⊢ Ⅎ x y ∈ A → ∀ x y ∈ A → x = y → φ ↔ y ∈ A → ∀ x x = y → φ
3 1 2 syl ⊢ Ⅎ _ x A → ∀ x y ∈ A → x = y → φ ↔ y ∈ A → ∀ x x = y → φ
4 3 albidv ⊢ Ⅎ _ x A → ∀ y ∀ x y ∈ A → x = y → φ ↔ ∀ y y ∈ A → ∀ x x = y → φ
5 wl-dfralflem ⊢ ∀ y ∀ x y ∈ A → x = y → φ ↔ ∀ x x ∈ A → φ
6 5 bicomi ⊢ ∀ x x ∈ A → φ ↔ ∀ y ∀ x y ∈ A → x = y → φ
7 df-wl-ral ⊢ ∀ x : A φ ↔ ∀ y y ∈ A → ∀ x x = y → φ
8 4 6 7 3bitr4g ⊢ Ⅎ _ x A → ∀ x x ∈ A → φ ↔ ∀ x : A φ
9 8 bicomd ⊢ Ⅎ _ x A → ∀ x : A φ ↔ ∀ x x ∈ A → φ