Theorem nfre1 3283

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

Syntax hints:   ∧ wa 397  ∃wex 1782  Ⅎwnf 1786   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-rex 3072

This theorem is referenced by:  2rmorex  3751  2reurex  3757  reuan  3891  2reu4lem  4526  nfiu1  5032  reusv2lem3  5399  fvelimad  6960  fsnex  7281  eusvobj2  7401  fiun  7929  f1iun  7930  zfregcl  9589  scott0  9881  ac6c4  10476  lbzbi  12920  mreiincl  17540  lss1d  20574  neiptopnei  22636  neitr  22684  utopsnneiplem  23752  cfilucfil  24068  2sqmo  26940  nosupbnd2  27219  noinfbnd2  27234  mptelee  28153  isch3  30494  atom1d  31606  opreu2reuALT  31717  iinabrex  31800  xrofsup  31980  locfinreflem  32820  esumc  33049  esumrnmpt2  33066  hasheuni  33083  esumcvg  33084  esumcvgre  33089  voliune  33227  volfiniune  33228  ddemeas  33234  eulerpartlemgvv  33375  bnj900  33940  bnj1189  34020  bnj1204  34023  bnj1398  34045  bnj1444  34054  bnj1445  34055  bnj1446  34056  bnj1447  34057  bnj1467  34065  bnj1518  34075  bnj1519  34076  iooelexlt  36243  fvineqsneq  36293  ptrest  36487  poimirlem26  36514  indexa  36601  filbcmb  36608  sdclem1  36611  heibor1  36678  dihglblem5  40169  unielss  41967  oaun3lem1  42124  suprnmpt  43870  disjinfi  43891  upbdrech  44015  ssfiunibd  44019  infxrunb2  44078  supxrunb3  44109  iccshift  44231  iooshift  44235  islpcn  44355  limsupre  44357  limclner  44367  limsupre3uzlem  44451  climuzlem  44459  xlimmnfv  44550  xlimpnfv  44554  itgperiod  44697  stoweidlem53  44769  stoweidlem57  44773  fourierdlem48  44870  fourierdlem51  44873  fourierdlem73  44895  fourierdlem81  44903  elaa2  44950  etransclem32  44982  sge0iunmptlemre  45131  voliunsge0lem  45188  meaiuninc3v  45200  isomenndlem  45246  ovnsubaddlem1  45286  hoidmvlelem1  45311  hoidmvlelem5  45315  smfaddlem1  45479  tworepnotupword  45600  2reu7  45819  2reu8  45820  f1oresf1o2  45999  mogoldbb  46453  2zrngagrp  46841  2zrngmmgm  46844