Theorem nfre1 3306

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

Syntax hints:   ∧ wa 398  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2145

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785  df-rex 3144

This theorem is referenced by:  r19.29anOLD  3332  2rmorex  3745  2reurex  3750  reuan  3880  2reu4lem  4465  nfiu1  4953  reusv2lem3  5301  fvelimad  6732  fsnex  7039  eusvobj2  7149  fiun  7644  f1iun  7645  zfregcl  9058  scott0  9315  ac6c4  9903  lbzbi  12337  mreiincl  16867  lss1d  19735  neiptopnei  21740  neitr  21788  utopsnneiplem  22856  cfilucfil  23169  2sqmo  26013  mptelee  26681  isch3  29018  atom1d  30130  opreu2reuALT  30240  xrofsup  30492  locfinreflem  31104  esumc  31310  esumrnmpt2  31327  hasheuni  31344  esumcvg  31345  esumcvgre  31350  voliune  31488  volfiniune  31489  ddemeas  31495  eulerpartlemgvv  31634  bnj900  32201  bnj1189  32281  bnj1204  32284  bnj1398  32306  bnj1444  32315  bnj1445  32316  bnj1446  32317  bnj1447  32318  bnj1467  32326  bnj1518  32336  bnj1519  32337  nosupbnd2  33216  iooelexlt  34646  fvineqsneq  34696  ptrest  34906  poimirlem26  34933  indexa  35023  filbcmb  35030  sdclem1  35033  heibor1  35103  dihglblem5  38449  suprnmpt  41450  disjinfi  41474  upbdrech  41592  ssfiunibd  41596  infxrunb2  41656  supxrunb3  41692  iccshift  41814  iooshift  41818  islpcn  41940  limsupre  41942  limclner  41952  limsupre3uzlem  42036  climuzlem  42044  xlimmnfv  42135  xlimpnfv  42139  itgperiod  42286  stoweidlem53  42358  stoweidlem57  42362  fourierdlem48  42459  fourierdlem51  42462  fourierdlem73  42484  fourierdlem81  42492  elaa2  42539  etransclem32  42571  sge0iunmptlemre  42717  voliunsge0lem  42774  meaiuninc3v  42786  isomenndlem  42832  ovnsubaddlem1  42872  hoidmvlelem1  42897  hoidmvlelem5  42901  smfaddlem1  43059  2reu7  43330  2reu8  43331  f1oresf1o2  43510  mogoldbb  43970  2zrngagrp  44234  2zrngmmgm  44237