Theorem nfre1 2884

Description: x is not free in E. x e. A ph. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfre1	|- F/ x E. x e. A ph

Proof of Theorem nfre1

Step	Hyp	Ref	Expression
1		df-rex 2801	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
2		nfe1 1780	. 2 |- F/ x E. x ( x e. A /\ ph )
3	1, 2	nfxfr 1616	1 |- F/ x E. x e. A ph

Syntax hints:   /\ wa 369   E.wex 1587   F/wnf 1590   e. wcel 1758   E.wrex 2796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-10 1777

This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591  df-rex 2801

This theorem is referenced by:  2rmorex  3264  nfiu1  4301  reusv2lem3  4596  eusvobj2  6186  fun11iun  6640  zfregcl  7913  scott0  8197  ac6c4  8754  lbzbi  11047  mreiincl  14645  lss1d  17159  neiptopnei  18861  neitr  18909  bwthOLD  19139  utopsnneiplem  19947  cfilucfilOLD  20269  cfilucfil  20270  restmetu  20287  colline  23187  f1otrg  23262  mptelee  23286  isch3  24789  atom1d  25902  xrofsup  26199  isarchi3  26342  ordtconlem1  26492  esumc  26643  hasheuni  26672  esumcvg  26673  voliune  26782  volfiniune  26783  ddemeas  26789  eulerpartlemgvv  26896  ptrest  28566  indexa  28768  filbcmb  28775  sdclem1  28780  heibor1  28850  infrglb  29912  stoweidlem53  29989  stoweidlem57  29993  reuan  30145  2reurex  30146  2reu4a  30154  2reu7  30156  2reu8  30157  bnj900  32225  bnj1189  32303  bnj1204  32306  bnj1398  32328  bnj1444  32337  bnj1445  32338  bnj1446  32339  bnj1447  32340  bnj1467  32348  bnj1518  32358  bnj1519  32359  dihglblem5  35252