Theorem nfre1 2848

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

Syntax hints:   /\ wa 371   E.wex 1663   F/wnf 1667   e. wcel 1887   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-10 1915

This theorem depends on definitions:  df-bi 189  df-ex 1664  df-nf 1668  df-rex 2743

This theorem is referenced by:  r19.29an  2931  2rmorex  3244  nfiu1  4308  reusv2lem3  4606  elsnxp  5378  fsnex  6181  eusvobj2  6283  fun11iun  6753  zfregcl  8109  scott0  8357  ac6c4  8911  lbzbi  11252  mreiincl  15502  lss1d  18186  neiptopnei  20148  neitr  20196  utopsnneiplem  21262  cfilucfil  21574  mptelee  24925  isch3  26894  atom1d  28006  xrofsup  28353  2sqmo  28410  locfinreflem  28667  esumc  28872  esumrnmpt2  28889  hasheuni  28906  esumcvg  28907  esumcvgre  28912  voliune  29052  volfiniune  29053  ddemeas  29059  eulerpartlemgvv  29209  bnj900  29740  bnj1189  29818  bnj1204  29821  bnj1398  29843  bnj1444  29852  bnj1445  29853  bnj1446  29854  bnj1447  29855  bnj1467  29863  bnj1518  29873  bnj1519  29874  iooelexlt  31765  ptrest  31939  poimirlem26  31966  indexa  32060  filbcmb  32067  sdclem1  32072  heibor1  32142  dihglblem5  34866  suprnmpt  37439  disjinfi  37468  upbdrech  37523  ssfiunibd  37527  iccshift  37619  iooshift  37623  infrglbOLD  37669  islpcn  37719  limsupre  37721  limsupreOLD  37722  limclner  37732  itgperiod  37858  stoweidlem53  37914  stoweidlem57  37918  fourierdlem48  38018  fourierdlem51  38021  fourierdlem73  38043  fourierdlem81  38051  elaa2  38099  etransclem32  38131  sge0iunmptlemre  38257  isomenndlem  38351  ovnsubaddlem1  38392  hoidmvlelem1  38417  hoidmvlelem5  38421  reuan  38601  2reurex  38602  2reu4a  38610  2reu7  38612  2reu8  38613  2zrngagrp  39996  2zrngmmgm  39999