Theorem nfre1 3244

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

Syntax hints:   ∧ wa 387  ∃wex 1743  Ⅎwnf 1747   ∈ wcel 2051  ∃wrex 3082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-10 2080

This theorem depends on definitions:  df-bi 199  df-ex 1744  df-nf 1748  df-rex 3087

This theorem is referenced by:  r19.29anOLD  3266  2rmorex  3647  2reurex  3652  reuan  3776  2reu4lem  4342  nfiu1  4819  reusv2lem3  5150  fvelimad  6559  fsnex  6862  eusvobj2  6967  fun11iun  7456  zfregcl  8851  scott0  9107  ac6c4  9699  lbzbi  12148  mreiincl  16737  lss1d  19469  neiptopnei  21459  neitr  21507  utopsnneiplem  22574  cfilucfil  22887  2sqmo  25730  mptelee  26399  isch3  28812  atom1d  29926  opreu2reuALT  30037  xrofsup  30268  locfinreflem  30780  esumc  30986  esumrnmpt2  31003  hasheuni  31020  esumcvg  31021  esumcvgre  31026  voliune  31165  volfiniune  31166  ddemeas  31172  eulerpartlemgvv  31311  bnj900  31880  bnj1189  31958  bnj1204  31961  bnj1398  31983  bnj1444  31992  bnj1445  31993  bnj1446  31994  bnj1447  31995  bnj1467  32003  bnj1518  32013  bnj1519  32014  nosupbnd2  32774  iooelexlt  34122  fvineqsneq  34171  ptrest  34369  poimirlem26  34396  indexa  34487  filbcmb  34494  sdclem1  34497  heibor1  34567  dihglblem5  37916  suprnmpt  40888  disjinfi  40912  upbdrech  41033  ssfiunibd  41037  infxrunb2  41097  supxrunb3  41134  iccshift  41257  iooshift  41261  islpcn  41383  limsupre  41385  limclner  41395  limsupre3uzlem  41479  climuzlem  41487  xlimmnfv  41578  xlimpnfv  41582  itgperiod  41728  stoweidlem53  41801  stoweidlem57  41805  fourierdlem48  41902  fourierdlem51  41905  fourierdlem73  41927  fourierdlem81  41935  elaa2  41982  etransclem32  42014  sge0iunmptlemre  42160  voliunsge0lem  42217  meaiuninc3v  42229  isomenndlem  42275  ovnsubaddlem1  42315  hoidmvlelem1  42340  hoidmvlelem5  42344  smfaddlem1  42502  2reu7  42748  2reu8  42749  f1oresf1o2  42928  mogoldbb  43350  2zrngagrp  43610  2zrngmmgm  43613