Theorem nfre1 3267

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

Syntax hints:   ∧ wa 395  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2108  ∃wrex 3060

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 2141

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

This theorem is referenced by:  2rmorex  3737  2reurex  3743  reuan  3871  2reu4lem  4497  nfiu1  5003  nfiu1OLD  5004  reusv2lem3  5370  fvelimad  6946  fsnex  7276  eusvobj2  7397  fiun  7941  f1iun  7942  zfregcl  9608  scott0  9900  ac6c4  10495  lbzbi  12952  mreiincl  17608  lss1d  20920  neiptopnei  23070  neitr  23118  utopsnneiplem  24186  cfilucfil  24498  2sqmo  27400  nosupbnd2  27680  noinfbnd2  27695  mptelee  28874  isch3  31222  atom1d  32334  opreu2reuALT  32458  iinabrex  32550  xrofsup  32744  locfinreflem  33871  esumc  34082  esumrnmpt2  34099  hasheuni  34116  esumcvg  34117  esumcvgre  34122  voliune  34260  volfiniune  34261  ddemeas  34267  eulerpartlemgvv  34408  bnj900  34960  bnj1189  35040  bnj1204  35043  bnj1398  35065  bnj1444  35074  bnj1445  35075  bnj1446  35076  bnj1447  35077  bnj1467  35085  bnj1518  35095  bnj1519  35096  iooelexlt  37380  fvineqsneq  37430  ptrest  37643  poimirlem26  37670  indexa  37757  filbcmb  37764  sdclem1  37767  heibor1  37834  dihglblem5  41317  unielss  43242  oaun3lem1  43398  suprnmpt  45198  disjinfi  45216  upbdrech  45334  ssfiunibd  45338  infxrunb2  45395  supxrunb3  45426  iccshift  45547  iooshift  45551  islpcn  45668  limsupre  45670  limclner  45680  limsupre3uzlem  45764  climuzlem  45772  xlimmnfv  45863  xlimpnfv  45867  itgperiod  46010  stoweidlem53  46082  stoweidlem57  46086  fourierdlem48  46183  fourierdlem51  46186  fourierdlem73  46208  fourierdlem81  46216  elaa2  46263  etransclem32  46295  sge0iunmptlemre  46444  voliunsge0lem  46501  meaiuninc3v  46513  isomenndlem  46559  ovnsubaddlem1  46599  hoidmvlelem1  46624  hoidmvlelem5  46628  smfaddlem1  46792  tworepnotupword  46915  2reu7  47140  2reu8  47141  f1oresf1o2  47320  mogoldbb  47799  2zrngagrp  48224  2zrngmmgm  48227