Theorem nfre1 2915

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 2810	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
2		nfe1 1845	. 2 |- F/ x E. x ( x e. A /\ ph )
3	1, 2	nfxfr 1650	1 |- F/ x E. x e. A ph

Syntax hints:   /\ wa 367   E.wex 1617   F/wnf 1621   e. wcel 1823   E.wrex 2805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-10 1842

This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622  df-rex 2810

This theorem is referenced by:  r19.29an  2995  2rmorex  3301  nfiu1  4345  reusv2lem3  4640  eusvobj2  6263  fun11iun  6733  zfregcl  8012  scott0  8295  ac6c4  8852  lbzbi  11171  mreiincl  15085  lss1d  17804  neiptopnei  19800  neitr  19848  utopsnneiplem  20916  cfilucfilOLD  21238  cfilucfil  21239  mptelee  24400  isch3  26357  atom1d  27470  elsnxp  27684  xrofsup  27816  2sqmo  27871  locfinreflem  28078  esumc  28280  esumrnmpt2  28297  hasheuni  28314  esumcvg  28315  esumcvgre  28320  voliune  28438  volfiniune  28439  ddemeas  28445  eulerpartlemgvv  28579  ptrest  30288  indexa  30464  filbcmb  30471  sdclem1  30476  heibor1  30546  suprnmpt  31691  upbdrech  31744  ssfiunibd  31748  iccshift  31797  iooshift  31801  infrglb  31823  islpcn  31884  limsupre  31886  limclner  31896  itgperiod  32019  stoweidlem53  32074  stoweidlem57  32078  fourierdlem48  32176  fourierdlem51  32179  fourierdlem73  32201  fourierdlem81  32209  elaa2  32256  etransclem32  32288  reuan  32424  2reurex  32425  2reu4a  32433  2reu7  32435  2reu8  32436  2zrngagrp  33003  2zrngmmgm  33006  bnj900  34388  bnj1189  34466  bnj1204  34469  bnj1398  34491  bnj1444  34500  bnj1445  34501  bnj1446  34502  bnj1447  34503  bnj1467  34511  bnj1518  34521  bnj1519  34522  dihglblem5  37422