Theorem nfre1 3005

Description: The setvar 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 2918	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
2		nfe1 2027	. 2 |- F/ x E. x ( x e. A /\ ph )
3	1, 2	nfxfr 1779	1 |- F/ x E. x e. A ph

Syntax hints:   /\ wa 384   E.wex 1704   F/wnf 1708   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-10 2019

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710  df-rex 2918

This theorem is referenced by:  r19.29an  3077  2rmorex  3412  nfiu1  4550  reusv2lem3  4871  elsnxpOLD  5678  fsnex  6538  eusvobj2  6643  fun11iun  7126  zfregcl  8499  zfregclOLD  8501  scott0  8749  ac6c4  9303  lbzbi  11776  mreiincl  16256  lss1d  18963  neiptopnei  20936  neitr  20984  utopsnneiplem  22051  cfilucfil  22364  mptelee  25775  isch3  28098  atom1d  29212  xrofsup  29533  2sqmo  29649  locfinreflem  29907  esumc  30113  esumrnmpt2  30130  hasheuni  30147  esumcvg  30148  esumcvgre  30153  voliune  30292  volfiniune  30293  ddemeas  30299  eulerpartlemgvv  30438  bnj900  30999  bnj1189  31077  bnj1204  31080  bnj1398  31102  bnj1444  31111  bnj1445  31112  bnj1446  31113  bnj1447  31114  bnj1467  31122  bnj1518  31132  bnj1519  31133  nosupbnd2  31862  iooelexlt  33210  ptrest  33408  poimirlem26  33435  indexa  33528  filbcmb  33535  sdclem1  33539  heibor1  33609  dihglblem5  36587  suprnmpt  39355  disjinfi  39380  fvelimad  39458  upbdrech  39519  ssfiunibd  39523  infxrunb2  39584  supxrunb3  39623  iccshift  39744  iooshift  39748  islpcn  39871  limsupre  39873  limclner  39883  limsupre3uzlem  39967  climuzlem  39975  xlimmnfv  40060  xlimpnfv  40064  itgperiod  40197  stoweidlem53  40270  stoweidlem57  40274  fourierdlem48  40371  fourierdlem51  40374  fourierdlem73  40396  fourierdlem81  40404  elaa2  40451  etransclem32  40483  sge0iunmptlemre  40632  voliunsge0lem  40689  isomenndlem  40744  ovnsubaddlem1  40784  hoidmvlelem1  40809  hoidmvlelem5  40813  smfaddlem1  40971  reuan  41180  2reurex  41181  2reu4a  41189  2reu7  41191  2reu8  41192  mogoldbb  41673  2zrngagrp  41943  2zrngmmgm  41946