Theorem nfre1 3291

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

Syntax hints:   ∧ wa 395  ∃wex 1777  Ⅎwnf 1781   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782  df-rex 3077

This theorem is referenced by:  2rmorex  3776  2reurex  3782  reuan  3918  2reu4lem  4545  nfiu1  5050  nfiu1OLD  5051  reusv2lem3  5418  fvelimad  6989  fsnex  7319  eusvobj2  7440  fiun  7983  f1iun  7984  zfregcl  9663  scott0  9955  ac6c4  10550  lbzbi  13001  mreiincl  17654  lss1d  20984  neiptopnei  23161  neitr  23209  utopsnneiplem  24277  cfilucfil  24593  2sqmo  27499  nosupbnd2  27779  noinfbnd2  27794  mptelee  28928  isch3  31273  atom1d  32385  opreu2reuALT  32505  iinabrex  32591  xrofsup  32774  locfinreflem  33786  esumc  34015  esumrnmpt2  34032  hasheuni  34049  esumcvg  34050  esumcvgre  34055  voliune  34193  volfiniune  34194  ddemeas  34200  eulerpartlemgvv  34341  bnj900  34905  bnj1189  34985  bnj1204  34988  bnj1398  35010  bnj1444  35019  bnj1445  35020  bnj1446  35021  bnj1447  35022  bnj1467  35030  bnj1518  35040  bnj1519  35041  iooelexlt  37328  fvineqsneq  37378  ptrest  37579  poimirlem26  37606  indexa  37693  filbcmb  37700  sdclem1  37703  heibor1  37770  dihglblem5  41255  unielss  43179  oaun3lem1  43336  suprnmpt  45081  disjinfi  45099  upbdrech  45220  ssfiunibd  45224  infxrunb2  45283  supxrunb3  45314  iccshift  45436  iooshift  45440  islpcn  45560  limsupre  45562  limclner  45572  limsupre3uzlem  45656  climuzlem  45664  xlimmnfv  45755  xlimpnfv  45759  itgperiod  45902  stoweidlem53  45974  stoweidlem57  45978  fourierdlem48  46075  fourierdlem51  46078  fourierdlem73  46100  fourierdlem81  46108  elaa2  46155  etransclem32  46187  sge0iunmptlemre  46336  voliunsge0lem  46393  meaiuninc3v  46405  isomenndlem  46451  ovnsubaddlem1  46491  hoidmvlelem1  46516  hoidmvlelem5  46520  smfaddlem1  46684  tworepnotupword  46805  2reu7  47026  2reu8  47027  f1oresf1o2  47206  mogoldbb  47659  2zrngagrp  47972  2zrngmmgm  47975