Theorem nfre1 3291

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

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

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 2180

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

This theorem is used by:  2rmorex  3715  2reurex  3721  reuan  3848  2reu4lem  4482  nfiu1  4991  reusv2lem3  5369  fvelimad  6983  fsnex  7322  eusvobj2  7443  fiun  7989  f1iun  7990  zfregclOLD  9626  scott0b  9974  scott0OLD  9975  ac6c4  10598  lbzbi  13103  mreiincl  17816  lss1d  21289  neiptopnei  23505  neitr  23553  utopsnneiplem  24621  cfilucfil  24933  2sqmo  27821  nosupbnd2  28130  noinfbnd2  28145  mpteleeOLD  29530  isch3  31900  atom1d  33012  opreu2reuALT  33172  iinabrex  33261  xrofsup  33455  locfinreflem  34583  esumc  34794  esumrnmpt2  34811  hasheuni  34828  esumcvg  34829  esumcvgre  34834  voliune  34973  volfiniune  34974  ddemeas  34980  eulerpartlemgvv  35119  bnj900  35670  bnj1189  35750  bnj1204  35753  bnj1398  35775  bnj1444  35784  bnj1445  35785  bnj1446  35786  bnj1447  35787  bnj1467  35795  bnj1518  35805  bnj1519  35806  srepdf  36128  iooelexlt  38553  fvineqsneq  38603  ptrest  38805  poimirlem26  38832  indexa  38935  filbcmb  38940  sdclem1  38943  heibor1  39010  dihglblem5  42621  unielss  44481  oaun3lem1  44637  suprnmpt  46462  disjinfi  46480  upbdrech  46594  ssfiunibd  46598  infxrunb2  46652  supxrunb3  46683  iccshift  46803  iooshift  46807  islpcn  46922  limsupre  46924  limclner  46934  limsupre3uzlem  47018  climuzlem  47026  xlimmnfv  47117  xlimpnfv  47121  itgperiod  47264  stoweidlem53  47336  stoweidlem57  47340  fourierdlem48  47437  fourierdlem51  47440  fourierdlem73  47462  fourierdlem81  47470  elaa2  47517  etransclem32  47549  sge0iunmptlemre  47698  voliunsge0lem  47755  meaiuninc3v  47767  isomenndlem  47813  ovnsubaddlem1  47853  hoidmvlelem1  47878  hoidmvlelem5  47882  smfaddlem1  48046  2reu7  48455  2reu8  48456  f1oresf1o2  48634  mogoldbb  49156  2zrngagrp  49619  2zrngmmgm  49622