Theorem nfe1 1520

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

Syntax hints:   F/wnf 1484   E.wex 1516

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 1473  ax-ie1 1517

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

This theorem is referenced by:  nf3  1693  sb4or  1857  nfmo1  2067  euexex  2141  2moswapdc  2146  nfre1  2551  ceqsexg  2908  morex  2964  sbc6g  3030  intab  3928  nfopab1  4129  nfopab2  4130  copsexg  4306  copsex2t  4307  copsex2g  4308  eusv2nf  4521  onintonm  4583  mosubopt  4758  dmcoss  4967  imadif  5373  funimaexglem  5376  nfoprab1  6017  nfoprab2  6018  nfoprab3  6019  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  dfgrp3mlem  13545