Theorem nfre1 3287

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

Syntax hints:   ∧ wa 399  ∃wex 1799  Ⅎwnf 1803   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-10 2175

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-nf 1804  df-rex 3087

This theorem is referenced by:  2rmorex  3717  2reurex  3723  reuan  3849  2reu4lem  4477  nfiu1  4985  reusv2lem3  5357  fvelimad  6934  fsnex  7267  eusvobj2  7388  fiun  7924  f1iun  7925  zfregclOLD  9543  scott0  9844  ac6c4  10438  lbzbi  12937  mreiincl  17624  lss1d  21027  neiptopnei  23189  neitr  23237  utopsnneiplem  24304  cfilucfil  24616  2sqmo  27498  nosupbnd2  27777  noinfbnd2  27792  mpteleeOLD  29093  isch3  31441  atom1d  32553  opreu2reuALT  32673  iinabrex  32766  xrofsup  32966  locfinreflem  34134  esumc  34345  esumrnmpt2  34362  hasheuni  34379  esumcvg  34380  esumcvgre  34385  voliune  34523  volfiniune  34524  ddemeas  34530  eulerpartlemgvv  34670  bnj900  35221  bnj1189  35301  bnj1204  35304  bnj1398  35326  bnj1444  35335  bnj1445  35336  bnj1446  35337  bnj1447  35338  bnj1467  35346  bnj1518  35356  bnj1519  35357  iooelexlt  37853  fvineqsneq  37903  ptrest  38115  poimirlem26  38142  indexa  38229  filbcmb  38236  sdclem1  38239  heibor1  38306  dihglblem5  41919  unielss  43792  oaun3lem1  43948  suprnmpt  45749  disjinfi  45767  upbdrech  45881  ssfiunibd  45885  infxrunb2  45940  supxrunb3  45971  iccshift  46091  iooshift  46095  islpcn  46210  limsupre  46212  limclner  46222  limsupre3uzlem  46306  climuzlem  46314  xlimmnfv  46405  xlimpnfv  46409  itgperiod  46552  stoweidlem53  46624  stoweidlem57  46628  fourierdlem48  46725  fourierdlem51  46728  fourierdlem73  46750  fourierdlem81  46758  elaa2  46805  etransclem32  46837  sge0iunmptlemre  46986  voliunsge0lem  47043  meaiuninc3v  47055  isomenndlem  47101  ovnsubaddlem1  47141  hoidmvlelem1  47166  hoidmvlelem5  47170  smfaddlem1  47334  2reu7  47702  2reu8  47703  f1oresf1o2  47882  mogoldbb  48404  2zrngagrp  48868  2zrngmmgm  48871