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 φ


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 syl5bb x y φ x φ x y φ y x φ