Metamath Proof Explorer

Theorem wl-sbnf1

Description: Two ways expressing that x is effectively not free in ph . Simplified version of sbnf2 . Note: This theorem shows that sbnf2 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019)

Ref Expression
Assertion wl-sbnf1 ⊢ ∀ x Ⅎ y φ → Ⅎ x φ ↔ ∀ x ∀ y φ → y x φ

Proof

Step Hyp Ref Expression
1 nf5 ⊢ Ⅎ x φ ↔ ∀ x φ → ∀ x φ
2 nfa1 ⊢ Ⅎ x ∀ x Ⅎ y φ
3 wl-sbhbt ⊢ ∀ x Ⅎ y φ → φ → ∀ x φ ↔ ∀ y φ → y x φ
4 2 3 albid ⊢ ∀ x Ⅎ y φ → ∀ x φ → ∀ x φ ↔ ∀ x ∀ y φ → y x φ
5 1 4 bitrid ⊢ ∀ x Ⅎ y φ → Ⅎ x φ ↔ ∀ x ∀ y φ → y x φ