Theorem nfre1 2767

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

Syntax hints:   /\ wa 369   E.wex 1586   F/wnf 1589   e. wcel 1756   E.wrex 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-10 1775

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590  df-rex 2716

This theorem is referenced by:  2rmorex  3158  nfiu1  4195  reusv2lem3  4490  eusvobj2  6079  fun11iun  6532  zfregcl  7801  scott0  8085  ac6c4  8642  lbzbi  10935  mreiincl  14526  lss1d  17021  neiptopnei  18711  neitr  18759  bwthOLD  18989  utopsnneiplem  19797  cfilucfilOLD  20119  cfilucfil  20120  restmetu  20137  colline  23020  f1otrg  23068  mptelee  23092  isch3  24595  atom1d  25708  xrofsup  26006  isarchi3  26155  ordtconlem1  26306  esumc  26457  hasheuni  26486  esumcvg  26487  voliune  26597  volfiniune  26598  ddemeas  26604  eulerpartlemgvv  26711  ptrest  28378  indexa  28580  filbcmb  28587  sdclem1  28592  heibor1  28662  infrglb  29724  stoweidlem53  29801  stoweidlem57  29805  reuan  29957  2reurex  29958  2reu4a  29966  2reu7  29968  2reu8  29969  bnj900  31809  bnj1189  31887  bnj1204  31890  bnj1398  31912  bnj1444  31921  bnj1445  31922  bnj1446  31923  bnj1447  31924  bnj1467  31932  bnj1518  31942  bnj1519  31943  dihglblem5  34783