Theorem nfre1 3263

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

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

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 3055

This theorem is referenced by:  2rmorex  3728  2reurex  3734  reuan  3862  2reu4lem  4488  nfiu1  4994  nfiu1OLD  4995  reusv2lem3  5358  fvelimad  6931  fsnex  7261  eusvobj2  7382  fiun  7924  f1iun  7925  zfregcl  9554  scott0  9846  ac6c4  10441  lbzbi  12902  mreiincl  17564  lss1d  20876  neiptopnei  23026  neitr  23074  utopsnneiplem  24142  cfilucfil  24454  2sqmo  27355  nosupbnd2  27635  noinfbnd2  27650  mptelee  28829  isch3  31177  atom1d  32289  opreu2reuALT  32413  iinabrex  32505  xrofsup  32697  locfinreflem  33837  esumc  34048  esumrnmpt2  34065  hasheuni  34082  esumcvg  34083  esumcvgre  34088  voliune  34226  volfiniune  34227  ddemeas  34233  eulerpartlemgvv  34374  bnj900  34926  bnj1189  35006  bnj1204  35009  bnj1398  35031  bnj1444  35040  bnj1445  35041  bnj1446  35042  bnj1447  35043  bnj1467  35051  bnj1518  35061  bnj1519  35062  iooelexlt  37357  fvineqsneq  37407  ptrest  37620  poimirlem26  37647  indexa  37734  filbcmb  37741  sdclem1  37744  heibor1  37811  dihglblem5  41299  unielss  43214  oaun3lem1  43370  suprnmpt  45175  disjinfi  45193  upbdrech  45310  ssfiunibd  45314  infxrunb2  45371  supxrunb3  45402  iccshift  45523  iooshift  45527  islpcn  45644  limsupre  45646  limclner  45656  limsupre3uzlem  45740  climuzlem  45748  xlimmnfv  45839  xlimpnfv  45843  itgperiod  45986  stoweidlem53  46058  stoweidlem57  46062  fourierdlem48  46159  fourierdlem51  46162  fourierdlem73  46184  fourierdlem81  46192  elaa2  46239  etransclem32  46271  sge0iunmptlemre  46420  voliunsge0lem  46477  meaiuninc3v  46489  isomenndlem  46535  ovnsubaddlem1  46575  hoidmvlelem1  46600  hoidmvlelem5  46604  smfaddlem1  46768  tworepnotupword  46891  2reu7  47116  2reu8  47117  f1oresf1o2  47296  mogoldbb  47790  2zrngagrp  48241  2zrngmmgm  48244