Theorem nfe1 1494

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

Syntax hints:   F/wnf 1458   E.wex 1490

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 1447  ax-ie1 1491

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

This theorem is referenced by:  nf3  1667  sb4or  1831  nfmo1  2036  euexex  2109  2moswapdc  2114  nfre1  2518  ceqsexg  2863  morex  2919  sbc6g  2985  rgenm  3523  intab  3869  nfopab1  4067  nfopab2  4068  copsexg  4238  copsex2t  4239  copsex2g  4240  eusv2nf  4450  onintonm  4510  mosubopt  4685  dmcoss  4889  imadif  5288  funimaexglem  5291  nfoprab1  5914  nfoprab2  5915  nfoprab3  5916  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  dfgrp3mlem  12827