Theorem nfre1 3290

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

Syntax hints:   ∧ wa 400  ∃wex 1809  Ⅎwnf 1813   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-10 2176

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814  df-rex 3090

This theorem is referenced by:  2rmorex  3717  2reurex  3723  reuan  3850  2reu4lem  4484  nfiu1  4992  reusv2lem3  5371  fvelimad  6948  fsnex  7281  eusvobj2  7402  fiun  7936  f1iun  7937  zfregclOLD  9553  scott0  9856  ac6c4  10460  lbzbi  12955  mreiincl  17643  lss1d  21084  neiptopnei  23289  neitr  23337  utopsnneiplem  24404  cfilucfil  24716  2sqmo  27601  nosupbnd2  27880  noinfbnd2  27895  mpteleeOLD  29245  isch3  31593  atom1d  32705  opreu2reuALT  32823  iinabrex  32914  xrofsup  33112  locfinreflem  34230  esumc  34441  esumrnmpt2  34458  hasheuni  34475  esumcvg  34476  esumcvgre  34481  voliune  34619  volfiniune  34620  ddemeas  34626  eulerpartlemgvv  34766  bnj900  35317  bnj1189  35397  bnj1204  35400  bnj1398  35422  bnj1444  35431  bnj1445  35432  bnj1446  35433  bnj1447  35434  bnj1467  35442  bnj1518  35452  bnj1519  35453  iooelexlt  38008  fvineqsneq  38058  ptrest  38270  poimirlem26  38297  indexa  38384  filbcmb  38391  sdclem1  38394  heibor1  38461  dihglblem5  42072  unielss  43945  oaun3lem1  44101  suprnmpt  45892  disjinfi  45910  upbdrech  46024  ssfiunibd  46028  infxrunb2  46083  supxrunb3  46114  iccshift  46234  iooshift  46238  islpcn  46353  limsupre  46355  limclner  46365  limsupre3uzlem  46449  climuzlem  46457  xlimmnfv  46548  xlimpnfv  46552  itgperiod  46695  stoweidlem53  46767  stoweidlem57  46771  fourierdlem48  46868  fourierdlem51  46871  fourierdlem73  46893  fourierdlem81  46901  elaa2  46948  etransclem32  46980  sge0iunmptlemre  47129  voliunsge0lem  47186  meaiuninc3v  47198  isomenndlem  47244  ovnsubaddlem1  47284  hoidmvlelem1  47309  hoidmvlelem5  47313  smfaddlem1  47477  2reu7  47848  2reu8  47849  f1oresf1o2  48028  mogoldbb  48550  2zrngagrp  49014  2zrngmmgm  49017