Theorem nfre1 3263

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

Syntax hints:   ∧ wa 395  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786  df-rex 3063

This theorem is referenced by:  2rmorex  3701  2reurex  3707  reuan  3835  2reu4lem  4464  nfiu1  4970  nfiu1OLD  4971  reusv2lem3  5338  fvelimad  6902  fsnex  7232  eusvobj2  7353  fiun  7890  f1iun  7891  zfregclOLD  9504  scott0  9804  ac6c4  10397  lbzbi  12880  mreiincl  17552  lss1d  20952  neiptopnei  23110  neitr  23158  utopsnneiplem  24225  cfilucfil  24537  2sqmo  27417  nosupbnd2  27697  noinfbnd2  27712  mpteleeOLD  28981  isch3  31330  atom1d  32442  opreu2reuALT  32564  iinabrex  32657  xrofsup  32858  locfinreflem  34003  esumc  34214  esumrnmpt2  34231  hasheuni  34248  esumcvg  34249  esumcvgre  34254  voliune  34392  volfiniune  34393  ddemeas  34399  eulerpartlemgvv  34539  bnj900  35090  bnj1189  35170  bnj1204  35173  bnj1398  35195  bnj1444  35204  bnj1445  35205  bnj1446  35206  bnj1447  35207  bnj1467  35215  bnj1518  35225  bnj1519  35226  iooelexlt  37695  fvineqsneq  37745  ptrest  37957  poimirlem26  37984  indexa  38071  filbcmb  38078  sdclem1  38081  heibor1  38148  dihglblem5  41761  unielss  43667  oaun3lem1  43823  suprnmpt  45625  disjinfi  45643  upbdrech  45759  ssfiunibd  45763  infxrunb2  45818  supxrunb3  45849  iccshift  45969  iooshift  45973  islpcn  46088  limsupre  46090  limclner  46100  limsupre3uzlem  46184  climuzlem  46192  xlimmnfv  46283  xlimpnfv  46287  itgperiod  46430  stoweidlem53  46502  stoweidlem57  46506  fourierdlem48  46603  fourierdlem51  46606  fourierdlem73  46628  fourierdlem81  46636  elaa2  46683  etransclem32  46715  sge0iunmptlemre  46864  voliunsge0lem  46921  meaiuninc3v  46933  isomenndlem  46979  ovnsubaddlem1  47019  hoidmvlelem1  47044  hoidmvlelem5  47048  smfaddlem1  47212  2reu7  47574  2reu8  47575  f1oresf1o2  47754  mogoldbb  48276  2zrngagrp  48740  2zrngmmgm  48743