Theorem nfre1 3215

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

Syntax hints:   ∧ wa 399  ∃wex 1787  Ⅎwnf 1791   ∈ wcel 2112  ∃wrex 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-10 2143

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792  df-rex 3057

This theorem is referenced by:  2rmorex  3656  2reurex  3662  reuan  3795  2reu4lem  4423  nfiu1  4924  reusv2lem3  5278  fvelimad  6757  fsnex  7071  eusvobj2  7184  fiun  7694  f1iun  7695  zfregcl  9188  scott0  9467  ac6c4  10060  lbzbi  12497  mreiincl  17053  lss1d  19954  neiptopnei  21983  neitr  22031  utopsnneiplem  23099  cfilucfil  23411  2sqmo  26272  mptelee  26940  isch3  29276  atom1d  30388  opreu2reuALT  30498  iinabrex  30581  xrofsup  30764  locfinreflem  31458  esumc  31685  esumrnmpt2  31702  hasheuni  31719  esumcvg  31720  esumcvgre  31725  voliune  31863  volfiniune  31864  ddemeas  31870  eulerpartlemgvv  32009  bnj900  32576  bnj1189  32656  bnj1204  32659  bnj1398  32681  bnj1444  32690  bnj1445  32691  bnj1446  32692  bnj1447  32693  bnj1467  32701  bnj1518  32711  bnj1519  32712  nosupbnd2  33605  noinfbnd2  33620  iooelexlt  35219  fvineqsneq  35269  ptrest  35462  poimirlem26  35489  indexa  35577  filbcmb  35584  sdclem1  35587  heibor1  35654  dihglblem5  38998  suprnmpt  42324  disjinfi  42345  upbdrech  42458  ssfiunibd  42462  infxrunb2  42521  supxrunb3  42553  iccshift  42672  iooshift  42676  islpcn  42798  limsupre  42800  limclner  42810  limsupre3uzlem  42894  climuzlem  42902  xlimmnfv  42993  xlimpnfv  42997  itgperiod  43140  stoweidlem53  43212  stoweidlem57  43216  fourierdlem48  43313  fourierdlem51  43316  fourierdlem73  43338  fourierdlem81  43346  elaa2  43393  etransclem32  43425  sge0iunmptlemre  43571  voliunsge0lem  43628  meaiuninc3v  43640  isomenndlem  43686  ovnsubaddlem1  43726  hoidmvlelem1  43751  hoidmvlelem5  43755  smfaddlem1  43913  2reu7  44218  2reu8  44219  f1oresf1o2  44398  mogoldbb  44853  2zrngagrp  45117  2zrngmmgm  45120