Theorem nfa1

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

	Ref	Expression
Assertion	nfa1	$$⊢Ⅎx\forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		alex	$$⊢\forall x\phi \leftrightarrow \neg \exists x\neg \phi$$
2		nfe1	$$⊢Ⅎx\exists x\neg \phi$$
3	2	nfn	$$⊢Ⅎx\neg \exists x\neg \phi$$
4	1 3	nfxfr	$$⊢Ⅎx\forall x\phi$$