Theorem nfre1 3264

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

Syntax hints:   ∧ wa 396  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2105  ∃wrex 3070

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 2136

This theorem depends on definitions:  df-bi 206  df-ex 1781  df-nf 1785  df-rex 3071

This theorem is referenced by:  2rmorex  3698  2reurex  3704  reuan  3838  2reu4lem  4467  nfiu1  4970  reusv2lem3  5337  fvelimad  6875  fsnex  7194  eusvobj2  7309  fiun  7831  f1iun  7832  zfregcl  9429  scott0  9721  ac6c4  10316  lbzbi  12755  mreiincl  17379  lss1d  20305  neiptopnei  22363  neitr  22411  utopsnneiplem  23479  cfilucfil  23795  2sqmo  26665  mptelee  27396  isch3  29735  atom1d  30847  opreu2reuALT  30957  iinabrex  31039  xrofsup  31221  locfinreflem  31926  esumc  32155  esumrnmpt2  32172  hasheuni  32189  esumcvg  32190  esumcvgre  32195  voliune  32333  volfiniune  32334  ddemeas  32340  eulerpartlemgvv  32479  bnj900  33044  bnj1189  33124  bnj1204  33127  bnj1398  33149  bnj1444  33158  bnj1445  33159  bnj1446  33160  bnj1447  33161  bnj1467  33169  bnj1518  33179  bnj1519  33180  nosupbnd2  33989  noinfbnd2  34004  iooelexlt  35610  fvineqsneq  35660  ptrest  35853  poimirlem26  35880  indexa  35968  filbcmb  35975  sdclem1  35978  heibor1  36045  dihglblem5  39538  suprnmpt  42956  disjinfi  42977  upbdrech  43098  ssfiunibd  43102  infxrunb2  43161  supxrunb3  43193  iccshift  43311  iooshift  43315  islpcn  43435  limsupre  43437  limclner  43447  limsupre3uzlem  43531  climuzlem  43539  xlimmnfv  43630  xlimpnfv  43634  itgperiod  43777  stoweidlem53  43849  stoweidlem57  43853  fourierdlem48  43950  fourierdlem51  43953  fourierdlem73  43975  fourierdlem81  43983  elaa2  44030  etransclem32  44062  sge0iunmptlemre  44209  voliunsge0lem  44266  meaiuninc3v  44278  isomenndlem  44324  ovnsubaddlem1  44364  hoidmvlelem1  44389  hoidmvlelem5  44393  smfaddlem1  44557  2reu7  44873  2reu8  44874  f1oresf1o2  45053  mogoldbb  45507  2zrngagrp  45771  2zrngmmgm  45774  tworepnotupword  46791