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

Metamath Proof Explorer

Theorem nfex

Description: If x is not free in ph , then it is not free in E. y ph . (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 30-Dec-2017) Reduce symbol count in nfex , hbex . (Revised by Wolf Lammen, 16-Oct-2021)

		Ref	Expression
	Hypothesis	nfex.1	$⊢ Ⅎ x φ$
	Assertion	nfex	$⊢ Ⅎ x \exists y φ$

Proof

Step	Hyp	Ref	Expression
1		nfex.1	$⊢ Ⅎ x φ$
2		df-ex	$⊢ \exists y φ \leftrightarrow \neg \forall y \neg φ$
3	1	nfn	$⊢ Ⅎ x \neg φ$
4	3	nfal	$⊢ Ⅎ x \forall y \neg φ$
5	4	nfn	$⊢ Ⅎ x \neg \forall y \neg φ$
6	2 5	nfxfr	$⊢ Ⅎ x \exists y φ$