Theorem nfre1 3263

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

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

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 3063

This theorem is referenced by:  2rmorex  3714  2reurex  3720  reuan  3848  2reu4lem  4478  nfiu1  4984  nfiu1OLD  4985  reusv2lem3  5347  fvelimad  6909  fsnex  7239  eusvobj2  7360  fiun  7897  f1iun  7898  zfregclOLD  9512  scott0  9810  ac6c4  10403  lbzbi  12861  mreiincl  17527  lss1d  20926  neiptopnei  23088  neitr  23136  utopsnneiplem  24203  cfilucfil  24515  2sqmo  27416  nosupbnd2  27696  noinfbnd2  27711  mpteleeOLD  28980  isch3  31329  atom1d  32441  opreu2reuALT  32563  iinabrex  32656  xrofsup  32858  locfinreflem  34018  esumc  34229  esumrnmpt2  34246  hasheuni  34263  esumcvg  34264  esumcvgre  34269  voliune  34407  volfiniune  34408  ddemeas  34414  eulerpartlemgvv  34554  bnj900  35105  bnj1189  35185  bnj1204  35188  bnj1398  35210  bnj1444  35219  bnj1445  35220  bnj1446  35221  bnj1447  35222  bnj1467  35230  bnj1518  35240  bnj1519  35241  iooelexlt  37617  fvineqsneq  37667  ptrest  37870  poimirlem26  37897  indexa  37984  filbcmb  37991  sdclem1  37994  heibor1  38061  dihglblem5  41674  unielss  43575  oaun3lem1  43731  suprnmpt  45533  disjinfi  45551  upbdrech  45667  ssfiunibd  45671  infxrunb2  45726  supxrunb3  45757  iccshift  45878  iooshift  45882  islpcn  45997  limsupre  45999  limclner  46009  limsupre3uzlem  46093  climuzlem  46101  xlimmnfv  46192  xlimpnfv  46196  itgperiod  46339  stoweidlem53  46411  stoweidlem57  46415  fourierdlem48  46512  fourierdlem51  46515  fourierdlem73  46537  fourierdlem81  46545  elaa2  46592  etransclem32  46624  sge0iunmptlemre  46773  voliunsge0lem  46830  meaiuninc3v  46842  isomenndlem  46888  ovnsubaddlem1  46928  hoidmvlelem1  46953  hoidmvlelem5  46957  smfaddlem1  47121  2reu7  47471  2reu8  47472  f1oresf1o2  47651  mogoldbb  48145  2zrngagrp  48609  2zrngmmgm  48612