Theorem nfre1 3288

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

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

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 2178

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

This theorem is used by:  2rmorex  3712  2reurex  3718  reuan  3844  2reu4lem  4479  nfiu1  4986  reusv2lem3  5362  fvelimad  6950  fsnex  7289  eusvobj2  7410  fiun  7953  f1iun  7954  zfregclOLD  9582  scott0b  9930  scott0OLD  9931  ac6c4  10552  lbzbi  13056  mreiincl  17759  lss1d  21231  neiptopnei  23443  neitr  23491  utopsnneiplem  24559  cfilucfil  24871  2sqmo  27757  nosupbnd2  28066  noinfbnd2  28081  mpteleeOLD  29466  isch3  31836  atom1d  32948  opreu2reuALT  33066  iinabrex  33156  xrofsup  33352  locfinreflem  34465  esumc  34676  esumrnmpt2  34693  hasheuni  34710  esumcvg  34711  esumcvgre  34716  voliune  34855  volfiniune  34856  ddemeas  34862  eulerpartlemgvv  35001  bnj900  35552  bnj1189  35632  bnj1204  35635  bnj1398  35657  bnj1444  35666  bnj1445  35667  bnj1446  35668  bnj1447  35669  bnj1467  35677  bnj1518  35687  bnj1519  35688  iooelexlt  38265  fvineqsneq  38315  ptrest  38517  poimirlem26  38544  indexa  38647  filbcmb  38654  sdclem1  38657  heibor1  38724  dihglblem5  42335  unielss  44204  oaun3lem1  44360  suprnmpt  46158  disjinfi  46176  upbdrech  46290  ssfiunibd  46294  infxrunb2  46348  supxrunb3  46379  iccshift  46499  iooshift  46503  islpcn  46618  limsupre  46620  limclner  46630  limsupre3uzlem  46714  climuzlem  46722  xlimmnfv  46813  xlimpnfv  46817  itgperiod  46960  stoweidlem53  47032  stoweidlem57  47036  fourierdlem48  47133  fourierdlem51  47136  fourierdlem73  47158  fourierdlem81  47166  elaa2  47213  etransclem32  47245  sge0iunmptlemre  47394  voliunsge0lem  47451  meaiuninc3v  47463  isomenndlem  47509  ovnsubaddlem1  47549  hoidmvlelem1  47574  hoidmvlelem5  47578  smfaddlem1  47742  2reu7  48150  2reu8  48151  f1oresf1o2  48330  mogoldbb  48852  2zrngagrp  49315  2zrngmmgm  49318