Theorem nfe1 1425

Description: x is not free in E. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfe1	|- F/ x E. x ph

Proof of Theorem nfe1

Step	Hyp	Ref	Expression
1		hbe1 1424	. 2 |- ( E. x ph -> A. x E. x ph )
2	1	nfi 1391	1 |- F/ x E. x ph

Syntax hints:   F/wnf 1389   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ie1 1422

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nf3  1599  sb4or  1754  nfmo1  1953  euexex  2026  2moswapdc  2031  nfre1  2407  ceqsexg  2723  morex  2776  sbc6g  2839  rgenm  3343  intab  3665  nfopab1  3847  nfopab2  3848  copsexg  3999  copsex2t  4000  copsex2g  4001  eusv2nf  4206  onintonm  4261  mosubopt  4423  dmcoss  4619  imadif  4999  funimaexglem  5002  nfoprab1  5574  nfoprab2  5575  nfoprab3  5576