Theorem nfre1 3261

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

Syntax hints:   ∧ wa 396  ∃wex 1778  Ⅎwnf 1782   ∈ wcel 2103  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-10 2134

This theorem depends on definitions:  df-bi 206  df-ex 1779  df-nf 1783  df-rex 3071

This theorem is referenced by:  2rmorex  3693  2reurex  3699  reuan  3833  2reu4lem  4460  nfiu1  4962  reusv2lem3  5327  fvelimad  6848  fsnex  7167  eusvobj2  7280  fiun  7797  f1iun  7798  zfregcl  9373  scott0  9664  ac6c4  10257  lbzbi  12696  mreiincl  17325  lss1d  20245  neiptopnei  22303  neitr  22351  utopsnneiplem  23419  cfilucfil  23735  2sqmo  26605  mptelee  27283  isch3  29623  atom1d  30735  opreu2reuALT  30845  iinabrex  30928  xrofsup  31110  locfinreflem  31810  esumc  32039  esumrnmpt2  32056  hasheuni  32073  esumcvg  32074  esumcvgre  32079  voliune  32217  volfiniune  32218  ddemeas  32224  eulerpartlemgvv  32363  bnj900  32929  bnj1189  33009  bnj1204  33012  bnj1398  33034  bnj1444  33043  bnj1445  33044  bnj1446  33045  bnj1447  33046  bnj1467  33054  bnj1518  33064  bnj1519  33065  nosupbnd2  33939  noinfbnd2  33954  iooelexlt  35553  fvineqsneq  35603  ptrest  35796  poimirlem26  35823  indexa  35911  filbcmb  35918  sdclem1  35921  heibor1  35988  dihglblem5  39330  suprnmpt  42734  disjinfi  42755  upbdrech  42872  ssfiunibd  42876  infxrunb2  42935  supxrunb3  42967  iccshift  43085  iooshift  43089  islpcn  43209  limsupre  43211  limclner  43221  limsupre3uzlem  43305  climuzlem  43313  xlimmnfv  43404  xlimpnfv  43408  itgperiod  43551  stoweidlem53  43623  stoweidlem57  43627  fourierdlem48  43724  fourierdlem51  43727  fourierdlem73  43749  fourierdlem81  43757  elaa2  43804  etransclem32  43836  sge0iunmptlemre  43983  voliunsge0lem  44040  meaiuninc3v  44052  isomenndlem  44098  ovnsubaddlem1  44138  hoidmvlelem1  44163  hoidmvlelem5  44167  smfaddlem1  44331  2reu7  44637  2reu8  44638  f1oresf1o2  44817  mogoldbb  45271  2zrngagrp  45535  2zrngmmgm  45538  tworepnotupword  46555