Theorem nfe1 1428

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 1427	. 2 |- ( E. x ph -> A. x E. x ph )
2	1	nfi 1394	1 |- F/ x E. x ph

Syntax hints:   F/wnf 1392   E.wex 1424

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 1381  ax-ie1 1425

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

This theorem is referenced by:  nf3  1602  sb4or  1758  nfmo1  1957  euexex  2030  2moswapdc  2035  nfre1  2415  ceqsexg  2736  morex  2790  sbc6g  2853  rgenm  3371  intab  3700  nfopab1  3882  nfopab2  3883  copsexg  4045  copsex2t  4046  copsex2g  4047  eusv2nf  4252  onintonm  4307  mosubopt  4471  dmcoss  4670  imadif  5059  funimaexglem  5062  nfoprab1  5655  nfoprab2  5656  nfoprab3  5657  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773