Theorem nfre1 3287

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

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1811  Ⅎwnf 1815   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-10 2177

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816  df-rex 3087

This theorem is used by:  2rmorex  3711  2reurex  3717  reuan  3844  2reu4lem  4478  nfiu1  4985  reusv2lem3  5362  fvelimad  6957  fsnex  7295  eusvobj2  7416  fiun  7959  f1iun  7960  zfregclOLD  9596  scott0b  9944  scott0OLD  9945  ac6c4  10566  lbzbi  13070  mreiincl  17775  lss1d  21247  neiptopnei  23459  neitr  23507  utopsnneiplem  24575  cfilucfil  24887  2sqmo  27773  nosupbnd2  28082  noinfbnd2  28097  mpteleeOLD  29482  isch3  31852  atom1d  32964  opreu2reuALT  33124  iinabrex  33214  xrofsup  33409  locfinreflem  34522  esumc  34733  esumrnmpt2  34750  hasheuni  34767  esumcvg  34768  esumcvgre  34773  voliune  34912  volfiniune  34913  ddemeas  34919  eulerpartlemgvv  35058  bnj900  35609  bnj1189  35689  bnj1204  35692  bnj1398  35714  bnj1444  35723  bnj1445  35724  bnj1446  35725  bnj1447  35726  bnj1467  35734  bnj1518  35744  bnj1519  35745  srepdf  36010  iooelexlt  38394  fvineqsneq  38444  ptrest  38646  poimirlem26  38673  indexa  38776  filbcmb  38783  sdclem1  38786  heibor1  38853  dihglblem5  42464  unielss  44329  oaun3lem1  44485  suprnmpt  46297  disjinfi  46315  upbdrech  46429  ssfiunibd  46433  infxrunb2  46487  supxrunb3  46518  iccshift  46638  iooshift  46642  islpcn  46757  limsupre  46759  limclner  46769  limsupre3uzlem  46853  climuzlem  46861  xlimmnfv  46952  xlimpnfv  46956  itgperiod  47099  stoweidlem53  47171  stoweidlem57  47175  fourierdlem48  47272  fourierdlem51  47275  fourierdlem73  47297  fourierdlem81  47305  elaa2  47352  etransclem32  47384  sge0iunmptlemre  47533  voliunsge0lem  47590  meaiuninc3v  47602  isomenndlem  47648  ovnsubaddlem1  47688  hoidmvlelem1  47713  hoidmvlelem5  47717  smfaddlem1  47881  2reu7  48290  2reu8  48291  f1oresf1o2  48469  mogoldbb  48991  2zrngagrp  49454  2zrngmmgm  49457