Theorem nfre1 2988

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

Syntax hints:   ∧ wa 383  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-10 2006

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701  df-rex 2902

This theorem is referenced by:  r19.29an  3059  2rmorex  3379  nfiu1  4486  reusv2lem3  4797  elsnxpOLD  5595  fsnex  6438  eusvobj2  6542  fun11iun  7019  zfregcl  8382  zfregclOLD  8384  scott0  8632  ac6c4  9186  lbzbi  11652  mreiincl  16079  lss1d  18784  neiptopnei  20746  neitr  20794  utopsnneiplem  21861  cfilucfil  22174  mptelee  25575  isch3  27482  atom1d  28596  xrofsup  28923  2sqmo  28980  locfinreflem  29235  esumc  29440  esumrnmpt2  29457  hasheuni  29474  esumcvg  29475  esumcvgre  29480  voliune  29619  volfiniune  29620  ddemeas  29626  eulerpartlemgvv  29765  bnj900  30253  bnj1189  30331  bnj1204  30334  bnj1398  30356  bnj1444  30365  bnj1445  30366  bnj1446  30367  bnj1447  30368  bnj1467  30376  bnj1518  30386  bnj1519  30387  iooelexlt  32386  ptrest  32578  poimirlem26  32605  indexa  32698  filbcmb  32705  sdclem1  32709  heibor1  32779  dihglblem5  35605  suprnmpt  38350  disjinfi  38375  upbdrech  38460  ssfiunibd  38464  infxrunb2  38525  iccshift  38591  iooshift  38595  islpcn  38706  limsupre  38708  limclner  38718  itgperiod  38873  stoweidlem53  38946  stoweidlem57  38950  fourierdlem48  39047  fourierdlem51  39050  fourierdlem73  39072  fourierdlem81  39080  elaa2  39127  etransclem32  39159  sge0iunmptlemre  39308  voliunsge0lem  39365  isomenndlem  39420  ovnsubaddlem1  39460  hoidmvlelem1  39485  hoidmvlelem5  39489  smfaddlem1  39649  reuan  39829  2reurex  39830  2reu4a  39838  2reu7  39840  2reu8  39841  2zrngagrp  41733  2zrngmmgm  41736