Theorem wl-nfalv

Description: If x is not present in ph , it is not free in A. y ph . (Contributed by Wolf Lammen, 11-Jan-2020)

	Ref	Expression
Assertion	wl-nfalv	⊢ Ⅎ 𝑥 ∀ 𝑦 𝜑

Proof

Step	Hyp	Ref	Expression
1		ax-5	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2	1	hbal	⊢ ( ∀ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜑 )
3	2	nf5i	⊢ Ⅎ 𝑥 ∀ 𝑦 𝜑