Theorem nfre1 2762

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

Syntax hints:   /\ wa 369   E.wex 1589   F/wnf 1592   e. wcel 1755   E.wrex 2706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-10 1774

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-nf 1593  df-rex 2711

This theorem is referenced by:  2rmorex  3152  nfiu1  4188  reusv2lem3  4483  eusvobj2  6072  fun11iun  6526  zfregcl  7797  scott0  8081  ac6c4  8638  lbzbi  10930  mreiincl  14516  lss1d  16965  neiptopnei  18577  neitr  18625  bwthOLD  18855  utopsnneiplem  19663  cfilucfilOLD  19985  cfilucfil  19986  restmetu  20003  colline  22917  f1otrg  22939  mptelee  22963  isch3  24466  atom1d  25579  xrofsup  25877  isarchi3  26027  ordtconlem1  26207  esumc  26358  hasheuni  26387  esumcvg  26388  voliune  26498  volfiniune  26499  ddemeas  26505  eulerpartlemgvv  26606  ptrest  28266  indexa  28468  filbcmb  28475  sdclem1  28480  heibor1  28550  infrglb  29614  stoweidlem53  29691  stoweidlem57  29695  reuan  29847  2reurex  29848  2reu4a  29856  2reu7  29858  2reu8  29859  bnj900  31621  bnj1189  31699  bnj1204  31702  bnj1398  31724  bnj1444  31733  bnj1445  31734  bnj1446  31735  bnj1447  31736  bnj1467  31744  bnj1518  31754  bnj1519  31755  dihglblem5  34513