Theorem nfre1 3282

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

Syntax hints:   ∧ wa 395  ∃wex 1775  Ⅎwnf 1779   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-10 2138

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-nf 1780  df-rex 3068

This theorem is referenced by:  2rmorex  3762  2reurex  3768  reuan  3904  2reu4lem  4527  nfiu1  5031  nfiu1OLD  5032  reusv2lem3  5405  fvelimad  6975  fsnex  7302  eusvobj2  7422  fiun  7965  f1iun  7966  zfregcl  9631  scott0  9923  ac6c4  10518  lbzbi  12975  mreiincl  17640  lss1d  20978  neiptopnei  23155  neitr  23203  utopsnneiplem  24271  cfilucfil  24587  2sqmo  27495  nosupbnd2  27775  noinfbnd2  27790  mptelee  28924  isch3  31269  atom1d  32381  opreu2reuALT  32504  iinabrex  32588  xrofsup  32777  locfinreflem  33800  esumc  34031  esumrnmpt2  34048  hasheuni  34065  esumcvg  34066  esumcvgre  34071  voliune  34209  volfiniune  34210  ddemeas  34216  eulerpartlemgvv  34357  bnj900  34921  bnj1189  35001  bnj1204  35004  bnj1398  35026  bnj1444  35035  bnj1445  35036  bnj1446  35037  bnj1447  35038  bnj1467  35046  bnj1518  35056  bnj1519  35057  iooelexlt  37344  fvineqsneq  37394  ptrest  37605  poimirlem26  37632  indexa  37719  filbcmb  37726  sdclem1  37729  heibor1  37796  dihglblem5  41280  unielss  43206  oaun3lem1  43363  suprnmpt  45116  disjinfi  45134  upbdrech  45255  ssfiunibd  45259  infxrunb2  45317  supxrunb3  45348  iccshift  45470  iooshift  45474  islpcn  45594  limsupre  45596  limclner  45606  limsupre3uzlem  45690  climuzlem  45698  xlimmnfv  45789  xlimpnfv  45793  itgperiod  45936  stoweidlem53  46008  stoweidlem57  46012  fourierdlem48  46109  fourierdlem51  46112  fourierdlem73  46134  fourierdlem81  46142  elaa2  46189  etransclem32  46221  sge0iunmptlemre  46370  voliunsge0lem  46427  meaiuninc3v  46439  isomenndlem  46485  ovnsubaddlem1  46525  hoidmvlelem1  46550  hoidmvlelem5  46554  smfaddlem1  46718  tworepnotupword  46839  2reu7  47060  2reu8  47061  f1oresf1o2  47240  mogoldbb  47709  2zrngagrp  48092  2zrngmmgm  48095