Theorem nfre1 3273

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

Syntax hints:   ∧ wa 394  ∃wex 1774  Ⅎwnf 1778   ∈ wcel 2099  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-10 2130

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779  df-rex 3061

This theorem is referenced by:  2rmorex  3748  2reurex  3754  reuan  3889  2reu4lem  4530  nfiu1  5035  nfiu1OLD  5036  reusv2lem3  5404  fvelimad  6970  fsnex  7297  eusvobj2  7416  fiun  7956  f1iun  7957  zfregcl  9637  scott0  9929  ac6c4  10524  lbzbi  12972  mreiincl  17609  lss1d  20940  neiptopnei  23127  neitr  23175  utopsnneiplem  24243  cfilucfil  24559  2sqmo  27466  nosupbnd2  27746  noinfbnd2  27761  mptelee  28829  isch3  31174  atom1d  32286  opreu2reuALT  32405  iinabrex  32489  xrofsup  32671  locfinreflem  33655  esumc  33884  esumrnmpt2  33901  hasheuni  33918  esumcvg  33919  esumcvgre  33924  voliune  34062  volfiniune  34063  ddemeas  34069  eulerpartlemgvv  34210  bnj900  34774  bnj1189  34854  bnj1204  34857  bnj1398  34879  bnj1444  34888  bnj1445  34889  bnj1446  34890  bnj1447  34891  bnj1467  34899  bnj1518  34909  bnj1519  34910  iooelexlt  37069  fvineqsneq  37119  ptrest  37320  poimirlem26  37347  indexa  37434  filbcmb  37441  sdclem1  37444  heibor1  37511  dihglblem5  40997  unielss  42883  oaun3lem1  43040  suprnmpt  44781  disjinfi  44799  upbdrech  44920  ssfiunibd  44924  infxrunb2  44983  supxrunb3  45014  iccshift  45136  iooshift  45140  islpcn  45260  limsupre  45262  limclner  45272  limsupre3uzlem  45356  climuzlem  45364  xlimmnfv  45455  xlimpnfv  45459  itgperiod  45602  stoweidlem53  45674  stoweidlem57  45678  fourierdlem48  45775  fourierdlem51  45778  fourierdlem73  45800  fourierdlem81  45808  elaa2  45855  etransclem32  45887  sge0iunmptlemre  46036  voliunsge0lem  46093  meaiuninc3v  46105  isomenndlem  46151  ovnsubaddlem1  46191  hoidmvlelem1  46216  hoidmvlelem5  46220  smfaddlem1  46384  tworepnotupword  46505  2reu7  46724  2reu8  46725  f1oresf1o2  46904  mogoldbb  47357  2zrngagrp  47626  2zrngmmgm  47629