Theorem nfre1 3234

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

Syntax hints:   ∧ wa 395  ∃wex 1783  Ⅎwnf 1787   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-10 2139

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788  df-rex 3069

This theorem is referenced by:  2rmorex  3684  2reurex  3690  reuan  3825  2reu4lem  4453  nfiu1  4955  reusv2lem3  5318  fvelimad  6818  fsnex  7135  eusvobj2  7248  fiun  7759  f1iun  7760  zfregcl  9283  scott0  9575  ac6c4  10168  lbzbi  12605  mreiincl  17222  lss1d  20140  neiptopnei  22191  neitr  22239  utopsnneiplem  23307  cfilucfil  23621  2sqmo  26490  mptelee  27166  isch3  29504  atom1d  30616  opreu2reuALT  30726  iinabrex  30809  xrofsup  30992  locfinreflem  31692  esumc  31919  esumrnmpt2  31936  hasheuni  31953  esumcvg  31954  esumcvgre  31959  voliune  32097  volfiniune  32098  ddemeas  32104  eulerpartlemgvv  32243  bnj900  32809  bnj1189  32889  bnj1204  32892  bnj1398  32914  bnj1444  32923  bnj1445  32924  bnj1446  32925  bnj1447  32926  bnj1467  32934  bnj1518  32944  bnj1519  32945  nosupbnd2  33846  noinfbnd2  33861  iooelexlt  35460  fvineqsneq  35510  ptrest  35703  poimirlem26  35730  indexa  35818  filbcmb  35825  sdclem1  35828  heibor1  35895  dihglblem5  39239  suprnmpt  42599  disjinfi  42620  upbdrech  42734  ssfiunibd  42738  infxrunb2  42797  supxrunb3  42829  iccshift  42946  iooshift  42950  islpcn  43070  limsupre  43072  limclner  43082  limsupre3uzlem  43166  climuzlem  43174  xlimmnfv  43265  xlimpnfv  43269  itgperiod  43412  stoweidlem53  43484  stoweidlem57  43488  fourierdlem48  43585  fourierdlem51  43588  fourierdlem73  43610  fourierdlem81  43618  elaa2  43665  etransclem32  43697  sge0iunmptlemre  43843  voliunsge0lem  43900  meaiuninc3v  43912  isomenndlem  43958  ovnsubaddlem1  43998  hoidmvlelem1  44023  hoidmvlelem5  44027  smfaddlem1  44185  2reu7  44490  2reu8  44491  f1oresf1o2  44670  mogoldbb  45125  2zrngagrp  45389  2zrngmmgm  45392