Theorem nfre1 2887

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

Syntax hints:   /\ wa 371   E.wex 1660   F/wnf 1664   e. wcel 1869   E.wrex 2777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-10 1888

This theorem depends on definitions:  df-bi 189  df-ex 1661  df-nf 1665  df-rex 2782

This theorem is referenced by:  r19.29an  2970  2rmorex  3277  nfiu1  4327  reusv2lem3  4625  elsnxp  5395  fsnex  6194  eusvobj2  6296  fun11iun  6765  zfregcl  8113  scott0  8360  ac6c4  8913  lbzbi  11254  mreiincl  15495  lss1d  18179  neiptopnei  20140  neitr  20188  utopsnneiplem  21254  cfilucfil  21566  mptelee  24917  isch3  26886  atom1d  27998  xrofsup  28353  2sqmo  28411  locfinreflem  28669  esumc  28874  esumrnmpt2  28891  hasheuni  28908  esumcvg  28909  esumcvgre  28914  voliune  29054  volfiniune  29055  ddemeas  29061  eulerpartlemgvv  29211  bnj900  29742  bnj1189  29820  bnj1204  29823  bnj1398  29845  bnj1444  29854  bnj1445  29855  bnj1446  29856  bnj1447  29857  bnj1467  29865  bnj1518  29875  bnj1519  29876  iooelexlt  31712  ptrest  31859  poimirlem26  31886  indexa  31980  filbcmb  31987  sdclem1  31992  heibor1  32062  dihglblem5  34791  suprnmpt  37294  disjinfi  37324  upbdrech  37371  ssfiunibd  37375  iccshift  37456  iooshift  37460  infrglbOLD  37495  islpcn  37545  limsupre  37547  limsupreOLD  37548  limclner  37558  itgperiod  37684  stoweidlem53  37740  stoweidlem57  37744  fourierdlem48  37844  fourierdlem51  37847  fourierdlem73  37869  fourierdlem81  37877  elaa2  37925  etransclem32  37957  sge0iunmptlemre  38051  isomenndlem  38136  ovnsubaddlem1  38173  reuan  38320  2reurex  38321  2reu4a  38329  2reu7  38331  2reu8  38332  2zrngagrp  39247  2zrngmmgm  39250