Theorem nfre1 3282

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

Syntax hints:   ∧ wa 396  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2137

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786  df-rex 3071

This theorem is referenced by:  2rmorex  3749  2reurex  3755  reuan  3889  2reu4lem  4524  nfiu1  5030  reusv2lem3  5397  fvelimad  6956  fsnex  7277  eusvobj2  7397  fiun  7925  f1iun  7926  zfregcl  9585  scott0  9877  ac6c4  10472  lbzbi  12916  mreiincl  17536  lss1d  20566  neiptopnei  22627  neitr  22675  utopsnneiplem  23743  cfilucfil  24059  2sqmo  26929  nosupbnd2  27208  noinfbnd2  27223  mptelee  28142  isch3  30481  atom1d  31593  opreu2reuALT  31704  iinabrex  31787  xrofsup  31967  locfinreflem  32808  esumc  33037  esumrnmpt2  33054  hasheuni  33071  esumcvg  33072  esumcvgre  33077  voliune  33215  volfiniune  33216  ddemeas  33222  eulerpartlemgvv  33363  bnj900  33928  bnj1189  34008  bnj1204  34011  bnj1398  34033  bnj1444  34042  bnj1445  34043  bnj1446  34044  bnj1447  34045  bnj1467  34053  bnj1518  34063  bnj1519  34064  iooelexlt  36231  fvineqsneq  36281  ptrest  36475  poimirlem26  36502  indexa  36589  filbcmb  36596  sdclem1  36599  heibor1  36666  dihglblem5  40157  unielss  41952  oaun3lem1  42109  suprnmpt  43855  disjinfi  43876  upbdrech  44001  ssfiunibd  44005  infxrunb2  44064  supxrunb3  44095  iccshift  44217  iooshift  44221  islpcn  44341  limsupre  44343  limclner  44353  limsupre3uzlem  44437  climuzlem  44445  xlimmnfv  44536  xlimpnfv  44540  itgperiod  44683  stoweidlem53  44755  stoweidlem57  44759  fourierdlem48  44856  fourierdlem51  44859  fourierdlem73  44881  fourierdlem81  44889  elaa2  44936  etransclem32  44968  sge0iunmptlemre  45117  voliunsge0lem  45174  meaiuninc3v  45186  isomenndlem  45232  ovnsubaddlem1  45272  hoidmvlelem1  45297  hoidmvlelem5  45301  smfaddlem1  45465  tworepnotupword  45586  2reu7  45805  2reu8  45806  f1oresf1o2  45985  mogoldbb  46439  2zrngagrp  46794  2zrngmmgm  46797