Theorem nfre1 3034

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

Syntax hints:   ∧ wa 383  ∃wex 1744  Ⅎwnf 1748   ∈ wcel 2030  ∃wrex 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-10 2059

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750  df-rex 2947

This theorem is referenced by:  r19.29an  3106  2rmorex  3445  nfiu1  4582  reusv2lem3  4901  elsnxpOLD  5716  fsnex  6578  eusvobj2  6683  fun11iun  7168  zfregcl  8540  scott0  8787  ac6c4  9341  lbzbi  11814  mreiincl  16303  lss1d  19011  neiptopnei  20984  neitr  21032  utopsnneiplem  22098  cfilucfil  22411  mptelee  25820  isch3  28226  atom1d  29340  xrofsup  29661  2sqmo  29777  locfinreflem  30035  esumc  30241  esumrnmpt2  30258  hasheuni  30275  esumcvg  30276  esumcvgre  30281  voliune  30420  volfiniune  30421  ddemeas  30427  eulerpartlemgvv  30566  bnj900  31125  bnj1189  31203  bnj1204  31206  bnj1398  31228  bnj1444  31237  bnj1445  31238  bnj1446  31239  bnj1447  31240  bnj1467  31248  bnj1518  31258  bnj1519  31259  nosupbnd2  31987  iooelexlt  33340  ptrest  33538  poimirlem26  33565  indexa  33658  filbcmb  33665  sdclem1  33669  heibor1  33739  dihglblem5  36904  suprnmpt  39669  disjinfi  39694  fvelimad  39772  upbdrech  39833  ssfiunibd  39837  infxrunb2  39897  supxrunb3  39936  iccshift  40062  iooshift  40066  islpcn  40189  limsupre  40191  limclner  40201  limsupre3uzlem  40285  climuzlem  40293  xlimmnfv  40378  xlimpnfv  40382  itgperiod  40515  stoweidlem53  40588  stoweidlem57  40592  fourierdlem48  40689  fourierdlem51  40692  fourierdlem73  40714  fourierdlem81  40722  elaa2  40769  etransclem32  40801  sge0iunmptlemre  40950  voliunsge0lem  41007  meaiuninc3v  41019  isomenndlem  41065  ovnsubaddlem1  41105  hoidmvlelem1  41130  hoidmvlelem5  41134  smfaddlem1  41292  reuan  41501  2reurex  41502  2reu4a  41510  2reu7  41512  2reu8  41513  mogoldbb  41998  2zrngagrp  42268  2zrngmmgm  42271