Theorem nfnf1

Description: The setvar x is not free in F/ x ph . (Contributed by Mario Carneiro, 11-Aug-2016) Remove dependency on ax-12 . (Revised by Wolf Lammen, 12-Oct-2021)

	Ref	Expression
Assertion	nfnf1	$$⊢ℲxℲx\phi$$

Proof

Step	Hyp	Ref	Expression
1		df-nf	$$⊢Ⅎx\phi \leftrightarrow \left(\exists x\phi \to \forall x\phi \right)$$
2		nfe1	$$⊢Ⅎx\exists x\phi$$
3		nfa1	$$⊢Ⅎx\forall x\phi$$
4	2 3	nfim	$$⊢Ⅎx\left(\exists x\phi \to \forall x\phi \right)$$
5	1 4	nfxfr	$$⊢ℲxℲx\phi$$