Theorem nfe1 1496

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

Syntax hints:   F/wnf 1460   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-ie1 1493

This theorem depends on definitions:  df-bi 117  df-nf 1461

This theorem is referenced by:  nf3  1669  sb4or  1833  nfmo1  2038  euexex  2111  2moswapdc  2116  nfre1  2520  ceqsexg  2865  morex  2921  sbc6g  2987  rgenm  3525  intab  3872  nfopab1  4070  nfopab2  4071  copsexg  4242  copsex2t  4243  copsex2g  4244  eusv2nf  4454  onintonm  4514  mosubopt  4689  dmcoss  4893  imadif  5293  funimaexglem  5296  nfoprab1  5919  nfoprab2  5920  nfoprab3  5921  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  dfgrp3mlem  12896