Theorem nfnf

Description: If x is not free in ph , it is not free in F/ y ph . (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 30-Dec-2017)

	Ref	Expression
Hypothesis	nfnf.1	$$⊢Ⅎx\phi$$
Assertion	nfnf	$$⊢ℲxℲy\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfnf.1	$$⊢Ⅎx\phi$$
2		df-nf	$$⊢Ⅎy\phi \leftrightarrow \left(\exists y\phi \to \forall y\phi \right)$$
3	1	nfex	$$⊢Ⅎx\exists y\phi$$
4	1	nfal	$$⊢Ⅎx\forall y\phi$$
5	3 4	nfim	$$⊢Ⅎx\left(\exists y\phi \to \forall y\phi \right)$$
6	2 5	nfxfr	$$⊢ℲxℲy\phi$$