Theorem nfre1 3262

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

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

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 3062

This theorem is referenced by:  2rmorex  3700  2reurex  3706  reuan  3834  2reu4lem  4463  nfiu1  4969  nfiu1OLD  4970  reusv2lem3  5342  fvelimad  6907  fsnex  7238  eusvobj2  7359  fiun  7896  f1iun  7897  zfregclOLD  9510  scott0  9810  ac6c4  10403  lbzbi  12886  mreiincl  17558  lss1d  20958  neiptopnei  23097  neitr  23145  utopsnneiplem  24212  cfilucfil  24524  2sqmo  27400  nosupbnd2  27680  noinfbnd2  27695  mpteleeOLD  28964  isch3  31312  atom1d  32424  opreu2reuALT  32546  iinabrex  32639  xrofsup  32840  locfinreflem  33984  esumc  34195  esumrnmpt2  34212  hasheuni  34229  esumcvg  34230  esumcvgre  34235  voliune  34373  volfiniune  34374  ddemeas  34380  eulerpartlemgvv  34520  bnj900  35071  bnj1189  35151  bnj1204  35154  bnj1398  35176  bnj1444  35185  bnj1445  35186  bnj1446  35187  bnj1447  35188  bnj1467  35196  bnj1518  35206  bnj1519  35207  iooelexlt  37678  fvineqsneq  37728  ptrest  37940  poimirlem26  37967  indexa  38054  filbcmb  38061  sdclem1  38064  heibor1  38131  dihglblem5  41744  unielss  43646  oaun3lem1  43802  suprnmpt  45604  disjinfi  45622  upbdrech  45738  ssfiunibd  45742  infxrunb2  45797  supxrunb3  45828  iccshift  45948  iooshift  45952  islpcn  46067  limsupre  46069  limclner  46079  limsupre3uzlem  46163  climuzlem  46171  xlimmnfv  46262  xlimpnfv  46266  itgperiod  46409  stoweidlem53  46481  stoweidlem57  46485  fourierdlem48  46582  fourierdlem51  46585  fourierdlem73  46607  fourierdlem81  46615  elaa2  46662  etransclem32  46694  sge0iunmptlemre  46843  voliunsge0lem  46900  meaiuninc3v  46912  isomenndlem  46958  ovnsubaddlem1  46998  hoidmvlelem1  47023  hoidmvlelem5  47027  smfaddlem1  47191  2reu7  47559  2reu8  47560  f1oresf1o2  47739  mogoldbb  48261  2zrngagrp  48725  2zrngmmgm  48728