Theorem nfre1 3292

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

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812  Ⅎwnf 1816   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2179

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817  df-rex 3092

This theorem is used by:  2rmorex  3719  2reurex  3725  reuan  3851  2reu4lem  4486  nfiu1  4994  reusv2lem3  5373  fvelimad  6952  fsnex  7290  eusvobj2  7411  fiun  7946  f1iun  7947  zfregclOLD  9564  scott0b  9873  scott0OLD  9874  ac6c4  10480  lbzbi  12976  mreiincl  17670  lss1d  21134  neiptopnei  23339  neitr  23387  utopsnneiplem  24455  cfilucfil  24767  2sqmo  27652  nosupbnd2  27931  noinfbnd2  27946  mpteleeOLD  29300  isch3  31664  atom1d  32776  opreu2reuALT  32894  iinabrex  32985  xrofsup  33182  locfinreflem  34294  esumc  34505  esumrnmpt2  34522  hasheuni  34539  esumcvg  34540  esumcvgre  34545  voliune  34684  volfiniune  34685  ddemeas  34691  eulerpartlemgvv  34831  bnj900  35382  bnj1189  35462  bnj1204  35465  bnj1398  35487  bnj1444  35496  bnj1445  35497  bnj1446  35498  bnj1447  35499  bnj1467  35507  bnj1518  35517  bnj1519  35518  iooelexlt  38065  fvineqsneq  38115  ptrest  38327  poimirlem26  38354  indexa  38442  filbcmb  38449  sdclem1  38452  heibor1  38519  dihglblem5  42130  unielss  44003  oaun3lem1  44159  suprnmpt  45950  disjinfi  45968  upbdrech  46082  ssfiunibd  46086  infxrunb2  46141  supxrunb3  46172  iccshift  46292  iooshift  46296  islpcn  46411  limsupre  46413  limclner  46423  limsupre3uzlem  46507  climuzlem  46515  xlimmnfv  46606  xlimpnfv  46610  itgperiod  46753  stoweidlem53  46825  stoweidlem57  46829  fourierdlem48  46926  fourierdlem51  46929  fourierdlem73  46951  fourierdlem81  46959  elaa2  47006  etransclem32  47038  sge0iunmptlemre  47187  voliunsge0lem  47244  meaiuninc3v  47256  isomenndlem  47302  ovnsubaddlem1  47342  hoidmvlelem1  47367  hoidmvlelem5  47371  smfaddlem1  47535  2reu7  47906  2reu8  47907  f1oresf1o2  48086  mogoldbb  48608  2zrngagrp  49071  2zrngmmgm  49074