Theorem nfex

Description: If x is not free in ph , 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	|- F/ x ph
Assertion	nfex	|- F/ x E. y ph

Proof

Step	Hyp	Ref	Expression
1		nfex.1	|- F/ x ph
2		df-ex	|- ( E. y ph <-> -. A. y -. ph )
3	1	nfn	|- F/ x -. ph
4	3	nfal	|- F/ x A. y -. ph
5	4	nfn	|- F/ x -. A. y -. ph
6	2 5	nfxfr	|- F/ x E. y ph