Theorem nfre1 3259

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 3059	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		nfe1 2155	. 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
3	1, 2	nfxfr 1854	1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑

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

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 3059

This theorem is referenced by:  2rmorex  3710  2reurex  3716  reuan  3844  2reu4lem  4474  nfiu1  4980  nfiu1OLD  4981  reusv2lem3  5343  fvelimad  6899  fsnex  7227  eusvobj2  7348  fiun  7885  f1iun  7886  zfregclOLD  9498  scott0  9796  ac6c4  10389  lbzbi  12847  mreiincl  17513  lss1d  20912  neiptopnei  23074  neitr  23122  utopsnneiplem  24189  cfilucfil  24501  2sqmo  27402  nosupbnd2  27682  noinfbnd2  27697  mpteleeOLD  28917  isch3  31265  atom1d  32377  opreu2reuALT  32500  iinabrex  32593  xrofsup  32796  locfinreflem  33946  esumc  34157  esumrnmpt2  34174  hasheuni  34191  esumcvg  34192  esumcvgre  34197  voliune  34335  volfiniune  34336  ddemeas  34342  eulerpartlemgvv  34482  bnj900  35034  bnj1189  35114  bnj1204  35117  bnj1398  35139  bnj1444  35148  bnj1445  35149  bnj1446  35150  bnj1447  35151  bnj1467  35159  bnj1518  35169  bnj1519  35170  iooelexlt  37506  fvineqsneq  37556  ptrest  37759  poimirlem26  37786  indexa  37873  filbcmb  37880  sdclem1  37883  heibor1  37950  dihglblem5  41497  unielss  43402  oaun3lem1  43558  suprnmpt  45360  disjinfi  45378  upbdrech  45495  ssfiunibd  45499  infxrunb2  45554  supxrunb3  45585  iccshift  45706  iooshift  45710  islpcn  45825  limsupre  45827  limclner  45837  limsupre3uzlem  45921  climuzlem  45929  xlimmnfv  46020  xlimpnfv  46024  itgperiod  46167  stoweidlem53  46239  stoweidlem57  46243  fourierdlem48  46340  fourierdlem51  46343  fourierdlem73  46365  fourierdlem81  46373  elaa2  46420  etransclem32  46452  sge0iunmptlemre  46601  voliunsge0lem  46658  meaiuninc3v  46670  isomenndlem  46716  ovnsubaddlem1  46756  hoidmvlelem1  46781  hoidmvlelem5  46785  smfaddlem1  46949  2reu7  47299  2reu8  47300  f1oresf1o2  47479  mogoldbb  47973  2zrngagrp  48437  2zrngmmgm  48440