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

Metamath Proof Explorer

Theorem nfri

Description: Consequence of the definition of not-free. (Contributed by Wolf Lammen, 16-Sep-2021)

		Ref	Expression
	Hypothesis	nfri.1	$⊢ Ⅎ x φ$
	Assertion	nfri	$⊢ \exists x φ \to \forall x φ$

Step	Hyp	Ref	Expression
1		nfri.1	$⊢ Ⅎ x φ$
2		df-nf	$⊢ Ⅎ x φ \leftrightarrow (\exists x φ \to \forall x φ)$
3	1 2	mpbi	$⊢ \exists x φ \to \forall x φ$