This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nf6

Description: An alternate definition of df-nf . (Contributed by Mario Carneiro, 24-Sep-2016)

		Ref	Expression
	Assertion	nf6	$⊢ Ⅎ x φ \leftrightarrow \forall x (\exists x φ \to φ)$

Step	Hyp	Ref	Expression
1		df-nf	$⊢ Ⅎ x φ \leftrightarrow (\exists x φ \to \forall x φ)$
2		nfe1	$⊢ Ⅎ x \exists x φ$
3	2	19.21	$⊢ \forall x (\exists x φ \to φ) \leftrightarrow (\exists x φ \to \forall x φ)$
4	1 3	bitr4i	$⊢ Ⅎ x φ \leftrightarrow \forall x (\exists x φ \to φ)$