Theorem nfe1 1483

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

Syntax hints:   F/wnf 1447   E.wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1436  ax-ie1 1480

This theorem depends on definitions:  df-bi 116  df-nf 1448

This theorem is referenced by:  nf3  1656  sb4or  1820  nfmo1  2025  euexex  2098  2moswapdc  2103  nfre1  2507  ceqsexg  2849  morex  2905  sbc6g  2970  rgenm  3506  intab  3847  nfopab1  4045  nfopab2  4046  copsexg  4216  copsex2t  4217  copsex2g  4218  eusv2nf  4428  onintonm  4488  mosubopt  4663  dmcoss  4867  imadif  5262  funimaexglem  5265  nfoprab1  5882  nfoprab2  5883  nfoprab3  5884  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150