Theorem nfe1 1549

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

Syntax hints:   F/wnf 1513   E.wex 1545

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 1502  ax-ie1 1546

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

This theorem is referenced by:  nf3  1721  sb4or  1886  nfmo1  2098  euexex  2172  2moswapdc  2177  nfre1  2593  ceqsexg  2954  morex  3010  sbc6g  3076  intab  3994  nfopab1  4195  nfopab2  4196  copsexg  4379  copsex2t  4380  copsex2g  4381  eusv2nf  4597  onintonm  4659  mosubopt  4835  dmcoss  5047  imadif  5456  funimaexglem  5459  nfoprab1  6127  nfoprab2  6128  nfoprab3  6129  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  dfgrp3mlem  13880