Theorem nfre1 2925

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

Syntax hints:   /\ wa 369   E.wex 1596   F/wnf 1599   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-10 1786

This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600  df-rex 2820

This theorem is referenced by:  r19.29an  3002  2rmorex  3308  nfiu1  4355  reusv2lem3  4650  eusvobj2  6275  fun11iun  6741  zfregcl  8016  scott0  8300  ac6c4  8857  lbzbi  11166  mreiincl  14847  lss1d  17392  neiptopnei  19399  neitr  19447  bwthOLD  19677  utopsnneiplem  20485  cfilucfilOLD  20807  cfilucfil  20808  restmetu  20825  colline  23743  f1otrg  23850  mptelee  23874  isch3  25835  atom1d  26948  xrofsup  27250  isarchi3  27393  ordtconlem1  27542  esumc  27702  hasheuni  27731  esumcvg  27732  voliune  27841  volfiniune  27842  ddemeas  27848  eulerpartlemgvv  27955  ptrest  29625  indexa  29827  filbcmb  29834  sdclem1  29839  heibor1  29909  suprnmpt  31029  upbdrech  31082  ssfiunibd  31086  iccshift  31122  iooshift  31126  infrglb  31140  islpcn  31181  limsupre  31183  limclner  31193  itgiccshift  31298  itgperiod  31299  stoweidlem53  31353  stoweidlem57  31357  fourierdlem48  31455  fourierdlem51  31458  fourierdlem73  31480  fourierdlem81  31488  reuan  31652  2reurex  31653  2reu4a  31661  2reu7  31663  2reu8  31664  bnj900  33066  bnj1189  33144  bnj1204  33147  bnj1398  33169  bnj1444  33178  bnj1445  33179  bnj1446  33180  bnj1447  33181  bnj1467  33189  bnj1518  33199  bnj1519  33200  dihglblem5  36095