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

Metamath Proof Explorer

Theorem nf5ri

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 15-Mar-2023)

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

Proof

Step	Hyp	Ref	Expression
1		nf5ri.1	$⊢ Ⅎ x φ$
2	1	nfri	$⊢ \exists x φ \to \forall x φ$
3	2	19.23bi	$⊢ φ \to \forall x φ$