Theorem nfre1 3287

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 2187	. 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
3	1, 2	nfxfr 1886	1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812  Ⅎwnf 1816   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2178

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817  df-rex 3087

This theorem is used by:  2rmorex  3712  2reurex  3718  reuan  3844  2reu4lem  4479  nfiu1  4986  reusv2lem3  5365  fvelimad  6945  fsnex  7284  eusvobj2  7405  fiun  7940  f1iun  7941  zfregclOLD  9567  scott0b  9876  scott0OLD  9877  ac6c4  10483  lbzbi  12985  mreiincl  17680  lss1d  21147  neiptopnei  23357  neitr  23405  utopsnneiplem  24473  cfilucfil  24785  2sqmo  27673  nosupbnd2  27952  noinfbnd2  27967  mpteleeOLD  29352  isch3  31722  atom1d  32834  opreu2reuALT  32952  iinabrex  33042  xrofsup  33238  locfinreflem  34350  esumc  34561  esumrnmpt2  34578  hasheuni  34595  esumcvg  34596  esumcvgre  34601  voliune  34740  volfiniune  34741  ddemeas  34747  eulerpartlemgvv  34887  bnj900  35438  bnj1189  35518  bnj1204  35521  bnj1398  35543  bnj1444  35552  bnj1445  35553  bnj1446  35554  bnj1447  35555  bnj1467  35563  bnj1518  35573  bnj1519  35574  iooelexlt  38116  fvineqsneq  38166  ptrest  38368  poimirlem26  38395  indexa  38483  filbcmb  38490  sdclem1  38493  heibor1  38560  dihglblem5  42171  unielss  44059  oaun3lem1  44215  suprnmpt  46006  disjinfi  46024  upbdrech  46138  ssfiunibd  46142  infxrunb2  46197  supxrunb3  46228  iccshift  46348  iooshift  46352  islpcn  46467  limsupre  46469  limclner  46479  limsupre3uzlem  46563  climuzlem  46571  xlimmnfv  46662  xlimpnfv  46666  itgperiod  46809  stoweidlem53  46881  stoweidlem57  46885  fourierdlem48  46982  fourierdlem51  46985  fourierdlem73  47007  fourierdlem81  47015  elaa2  47062  etransclem32  47094  sge0iunmptlemre  47243  voliunsge0lem  47300  meaiuninc3v  47312  isomenndlem  47358  ovnsubaddlem1  47398  hoidmvlelem1  47423  hoidmvlelem5  47427  smfaddlem1  47591  2reu7  47999  2reu8  48000  f1oresf1o2  48179  mogoldbb  48701  2zrngagrp  49164  2zrngmmgm  49167