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

Syntax hints:   ∧ wa 396  ∃wex 1786  Ⅎwnf 1790   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-10 2152

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791  df-rex 3064

This theorem is referenced by:  2rmorex  3695  2reurex  3701  reuan  3828  2reu4lem  4451  nfiu1  4957  reusv2lem3  5329  fvelimad  6894  fsnex  7227  eusvobj2  7348  fiun  7885  f1iun  7886  zfregclOLD  9500  scott0  9801  ac6c4  10394  lbzbi  12877  mreiincl  17549  lss1d  20953  neiptopnei  23115  neitr  23163  utopsnneiplem  24230  cfilucfil  24542  2sqmo  27418  nosupbnd2  27698  noinfbnd2  27713  mpteleeOLD  28982  isch3  31330  atom1d  32442  opreu2reuALT  32564  iinabrex  32658  xrofsup  32859  locfinreflem  34024  esumc  34235  esumrnmpt2  34252  hasheuni  34269  esumcvg  34270  esumcvgre  34275  voliune  34413  volfiniune  34414  ddemeas  34420  eulerpartlemgvv  34560  bnj900  35111  bnj1189  35191  bnj1204  35194  bnj1398  35216  bnj1444  35225  bnj1445  35226  bnj1446  35227  bnj1447  35228  bnj1467  35236  bnj1518  35246  bnj1519  35247  iooelexlt  37724  fvineqsneq  37774  ptrest  37986  poimirlem26  38013  indexa  38100  filbcmb  38107  sdclem1  38110  heibor1  38177  dihglblem5  41790  unielss  43663  oaun3lem1  43819  suprnmpt  45621  disjinfi  45639  upbdrech  45753  ssfiunibd  45757  infxrunb2  45812  supxrunb3  45843  iccshift  45963  iooshift  45967  islpcn  46082  limsupre  46084  limclner  46094  limsupre3uzlem  46178  climuzlem  46186  xlimmnfv  46277  xlimpnfv  46281  itgperiod  46424  stoweidlem53  46496  stoweidlem57  46500  fourierdlem48  46597  fourierdlem51  46600  fourierdlem73  46622  fourierdlem81  46630  elaa2  46677  etransclem32  46709  sge0iunmptlemre  46858  voliunsge0lem  46915  meaiuninc3v  46927  isomenndlem  46973  ovnsubaddlem1  47013  hoidmvlelem1  47038  hoidmvlelem5  47042  smfaddlem1  47206  2reu7  47574  2reu8  47575  f1oresf1o2  47754  mogoldbb  48276  2zrngagrp  48740  2zrngmmgm  48743