Theorem nfre1 3296

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

Syntax hints:   ∧ wa 400  ∃wex 1806  Ⅎwnf 1810   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-10 2182

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811  df-rex 3096

This theorem is referenced by:  2rmorex  3726  2reurex  3732  reuan  3858  2reu4lem  4489  nfiu1  4996  reusv2lem3  5372  fvelimad  6949  fsnex  7282  eusvobj2  7403  fiun  7939  f1iun  7940  zfregclOLD  9556  scott0  9859  ac6c4  10464  lbzbi  12959  mreiincl  17647  lss1d  21061  neiptopnei  23257  neitr  23305  utopsnneiplem  24372  cfilucfil  24684  2sqmo  27566  nosupbnd2  27845  noinfbnd2  27860  mpteleeOLD  29185  isch3  31533  atom1d  32645  opreu2reuALT  32763  iinabrex  32854  xrofsup  33052  locfinreflem  34174  esumc  34385  esumrnmpt2  34402  hasheuni  34419  esumcvg  34420  esumcvgre  34425  voliune  34563  volfiniune  34564  ddemeas  34570  eulerpartlemgvv  34710  bnj900  35261  bnj1189  35341  bnj1204  35344  bnj1398  35366  bnj1444  35375  bnj1445  35376  bnj1446  35377  bnj1447  35378  bnj1467  35386  bnj1518  35396  bnj1519  35397  iooelexlt  37895  fvineqsneq  37945  ptrest  38157  poimirlem26  38184  indexa  38271  filbcmb  38278  sdclem1  38281  heibor1  38348  dihglblem5  41961  unielss  43836  oaun3lem1  43992  suprnmpt  45783  disjinfi  45801  upbdrech  45915  ssfiunibd  45919  infxrunb2  45974  supxrunb3  46005  iccshift  46125  iooshift  46129  islpcn  46244  limsupre  46246  limclner  46256  limsupre3uzlem  46340  climuzlem  46348  xlimmnfv  46439  xlimpnfv  46443  itgperiod  46586  stoweidlem53  46658  stoweidlem57  46662  fourierdlem48  46759  fourierdlem51  46762  fourierdlem73  46784  fourierdlem81  46792  elaa2  46839  etransclem32  46871  sge0iunmptlemre  47020  voliunsge0lem  47077  meaiuninc3v  47089  isomenndlem  47135  ovnsubaddlem1  47175  hoidmvlelem1  47200  hoidmvlelem5  47204  smfaddlem1  47368  2reu7  47736  2reu8  47737  f1oresf1o2  47916  mogoldbb  48438  2zrngagrp  48902  2zrngmmgm  48905