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 
|- 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