Theorem nfre1 3254

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  3714  2reurex  3720  reuan  3848  2reu4lem  4473  nfiu1  4977  nfiu1OLD  4978  reusv2lem3  5339  fvelimad  6890  fsnex  7220  eusvobj2  7341  fiun  7878  f1iun  7879  zfregclOLD  9487  scott0  9782  ac6c4  10375  lbzbi  12837  mreiincl  17498  lss1d  20866  neiptopnei  23017  neitr  23065  utopsnneiplem  24133  cfilucfil  24445  2sqmo  27346  nosupbnd2  27626  noinfbnd2  27641  mptelee  28840  isch3  31185  atom1d  32297  opreu2reuALT  32421  iinabrex  32513  xrofsup  32710  locfinreflem  33807  esumc  34018  esumrnmpt2  34035  hasheuni  34052  esumcvg  34053  esumcvgre  34058  voliune  34196  volfiniune  34197  ddemeas  34203  eulerpartlemgvv  34344  bnj900  34896  bnj1189  34976  bnj1204  34979  bnj1398  35001  bnj1444  35010  bnj1445  35011  bnj1446  35012  bnj1447  35013  bnj1467  35021  bnj1518  35031  bnj1519  35032  iooelexlt  37336  fvineqsneq  37386  ptrest  37599  poimirlem26  37626  indexa  37713  filbcmb  37720  sdclem1  37723  heibor1  37790  dihglblem5  41277  unielss  43191  oaun3lem1  43347  suprnmpt  45152  disjinfi  45170  upbdrech  45287  ssfiunibd  45291  infxrunb2  45347  supxrunb3  45378  iccshift  45499  iooshift  45503  islpcn  45620  limsupre  45622  limclner  45632  limsupre3uzlem  45716  climuzlem  45724  xlimmnfv  45815  xlimpnfv  45819  itgperiod  45962  stoweidlem53  46034  stoweidlem57  46038  fourierdlem48  46135  fourierdlem51  46138  fourierdlem73  46160  fourierdlem81  46168  elaa2  46215  etransclem32  46247  sge0iunmptlemre  46396  voliunsge0lem  46453  meaiuninc3v  46465  isomenndlem  46511  ovnsubaddlem1  46551  hoidmvlelem1  46576  hoidmvlelem5  46580  smfaddlem1  46744  tworepnotupword  46867  2reu7  47095  2reu8  47096  f1oresf1o2  47275  mogoldbb  47769  2zrngagrp  48233  2zrngmmgm  48236