Theorem nfre1 3261

Description: The setvar 𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfre1	⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑

Proof of Theorem nfre1

Step	Hyp	Ref	Expression
1		df-rex 3061	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		nfe1 2155	. 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
3	1, 2	nfxfr 1854	1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∧ wa 395  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2146

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785  df-rex 3061

This theorem is referenced by:  2rmorex  3712  2reurex  3718  reuan  3846  2reu4lem  4476  nfiu1  4982  nfiu1OLD  4983  reusv2lem3  5345  fvelimad  6901  fsnex  7229  eusvobj2  7350  fiun  7887  f1iun  7888  zfregclOLD  9500  scott0  9798  ac6c4  10391  lbzbi  12849  mreiincl  17515  lss1d  20914  neiptopnei  23076  neitr  23124  utopsnneiplem  24191  cfilucfil  24503  2sqmo  27404  nosupbnd2  27684  noinfbnd2  27699  mpteleeOLD  28968  isch3  31316  atom1d  32428  opreu2reuALT  32551  iinabrex  32644  xrofsup  32847  locfinreflem  33997  esumc  34208  esumrnmpt2  34225  hasheuni  34242  esumcvg  34243  esumcvgre  34248  voliune  34386  volfiniune  34387  ddemeas  34393  eulerpartlemgvv  34533  bnj900  35085  bnj1189  35165  bnj1204  35168  bnj1398  35190  bnj1444  35199  bnj1445  35200  bnj1446  35201  bnj1447  35202  bnj1467  35210  bnj1518  35220  bnj1519  35221  iooelexlt  37567  fvineqsneq  37617  ptrest  37820  poimirlem26  37847  indexa  37934  filbcmb  37941  sdclem1  37944  heibor1  38011  dihglblem5  41558  unielss  43460  oaun3lem1  43616  suprnmpt  45418  disjinfi  45436  upbdrech  45553  ssfiunibd  45557  infxrunb2  45612  supxrunb3  45643  iccshift  45764  iooshift  45768  islpcn  45883  limsupre  45885  limclner  45895  limsupre3uzlem  45979  climuzlem  45987  xlimmnfv  46078  xlimpnfv  46082  itgperiod  46225  stoweidlem53  46297  stoweidlem57  46301  fourierdlem48  46398  fourierdlem51  46401  fourierdlem73  46423  fourierdlem81  46431  elaa2  46478  etransclem32  46510  sge0iunmptlemre  46659  voliunsge0lem  46716  meaiuninc3v  46728  isomenndlem  46774  ovnsubaddlem1  46814  hoidmvlelem1  46839  hoidmvlelem5  46843  smfaddlem1  47007  2reu7  47357  2reu8  47358  f1oresf1o2  47537  mogoldbb  48031  2zrngagrp  48495  2zrngmmgm  48498