Theorem nfre1 3260

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

Syntax hints:   ∧ wa 395  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-rex 3054

This theorem is referenced by:  2rmorex  3722  2reurex  3728  reuan  3856  2reu4lem  4481  nfiu1  4987  nfiu1OLD  4988  reusv2lem3  5350  fvelimad  6910  fsnex  7240  eusvobj2  7361  fiun  7901  f1iun  7902  zfregcl  9523  scott0  9815  ac6c4  10410  lbzbi  12871  mreiincl  17533  lss1d  20845  neiptopnei  22995  neitr  23043  utopsnneiplem  24111  cfilucfil  24423  2sqmo  27324  nosupbnd2  27604  noinfbnd2  27619  mptelee  28798  isch3  31143  atom1d  32255  opreu2reuALT  32379  iinabrex  32471  xrofsup  32663  locfinreflem  33803  esumc  34014  esumrnmpt2  34031  hasheuni  34048  esumcvg  34049  esumcvgre  34054  voliune  34192  volfiniune  34193  ddemeas  34199  eulerpartlemgvv  34340  bnj900  34892  bnj1189  34972  bnj1204  34975  bnj1398  34997  bnj1444  35006  bnj1445  35007  bnj1446  35008  bnj1447  35009  bnj1467  35017  bnj1518  35027  bnj1519  35028  iooelexlt  37323  fvineqsneq  37373  ptrest  37586  poimirlem26  37613  indexa  37700  filbcmb  37707  sdclem1  37710  heibor1  37777  dihglblem5  41265  unielss  43180  oaun3lem1  43336  suprnmpt  45141  disjinfi  45159  upbdrech  45276  ssfiunibd  45280  infxrunb2  45337  supxrunb3  45368  iccshift  45489  iooshift  45493  islpcn  45610  limsupre  45612  limclner  45622  limsupre3uzlem  45706  climuzlem  45714  xlimmnfv  45805  xlimpnfv  45809  itgperiod  45952  stoweidlem53  46024  stoweidlem57  46028  fourierdlem48  46125  fourierdlem51  46128  fourierdlem73  46150  fourierdlem81  46158  elaa2  46205  etransclem32  46237  sge0iunmptlemre  46386  voliunsge0lem  46443  meaiuninc3v  46455  isomenndlem  46501  ovnsubaddlem1  46541  hoidmvlelem1  46566  hoidmvlelem5  46570  smfaddlem1  46734  tworepnotupword  46857  2reu7  47085  2reu8  47086  f1oresf1o2  47265  mogoldbb  47759  2zrngagrp  48210  2zrngmmgm  48213