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

This proof depends on syntax axioms:   F/wnf 1513   E.wex 1545

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nf3  1721  sb4or  1886  nfmo1  2098  euexex  2172  2moswapdc  2177  nfre1  2593  ceqsexg  2954  morex  3010  sbc6g  3076  intab  3999  nfopab1  4200  nfopab2  4201  copsexg  4384  copsex2t  4385  copsex2g  4386  eusv2nf  4602  onintonm  4664  mosubopt  4840  dmcoss  5052  imadif  5461  funimaexglem  5464  nfoprab1  6137  nfoprab2  6138  nfoprab3  6139  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  dfgrp3mlem  13903