Theorem nfe1 1510

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

Syntax hints:   F/wnf 1474   E.wex 1506

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 1463  ax-ie1 1507

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

This theorem is referenced by:  nf3  1683  sb4or  1847  nfmo1  2057  euexex  2130  2moswapdc  2135  nfre1  2540  ceqsexg  2892  morex  2948  sbc6g  3014  intab  3903  nfopab1  4102  nfopab2  4103  copsexg  4277  copsex2t  4278  copsex2g  4279  eusv2nf  4491  onintonm  4553  mosubopt  4728  dmcoss  4935  imadif  5338  funimaexglem  5341  nfoprab1  5971  nfoprab2  5972  nfoprab3  5973  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  dfgrp3mlem  13230