Theorem nfre1 3260

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

Syntax hints:   ∧ wa 395  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-rex 3054

This theorem is referenced by:  2rmorex  3722  2reurex  3728  reuan  3856  2reu4lem  4481  nfiu1  4987  nfiu1OLD  4988  reusv2lem3  5350  fvelimad  6910  fsnex  7240  eusvobj2  7361  fiun  7901  f1iun  7902  zfregcl  9523  scott0  9815  ac6c4  10410  lbzbi  12871  mreiincl  17533  lss1d  20901  neiptopnei  23052  neitr  23100  utopsnneiplem  24168  cfilucfil  24480  2sqmo  27381  nosupbnd2  27661  noinfbnd2  27676  mptelee  28875  isch3  31220  atom1d  32332  opreu2reuALT  32456  iinabrex  32548  xrofsup  32740  locfinreflem  33823  esumc  34034  esumrnmpt2  34051  hasheuni  34068  esumcvg  34069  esumcvgre  34074  voliune  34212  volfiniune  34213  ddemeas  34219  eulerpartlemgvv  34360  bnj900  34912  bnj1189  34992  bnj1204  34995  bnj1398  35017  bnj1444  35026  bnj1445  35027  bnj1446  35028  bnj1447  35029  bnj1467  35037  bnj1518  35047  bnj1519  35048  iooelexlt  37343  fvineqsneq  37393  ptrest  37606  poimirlem26  37633  indexa  37720  filbcmb  37727  sdclem1  37730  heibor1  37797  dihglblem5  41285  unielss  43200  oaun3lem1  43356  suprnmpt  45161  disjinfi  45179  upbdrech  45296  ssfiunibd  45300  infxrunb2  45357  supxrunb3  45388  iccshift  45509  iooshift  45513  islpcn  45630  limsupre  45632  limclner  45642  limsupre3uzlem  45726  climuzlem  45734  xlimmnfv  45825  xlimpnfv  45829  itgperiod  45972  stoweidlem53  46044  stoweidlem57  46048  fourierdlem48  46145  fourierdlem51  46148  fourierdlem73  46170  fourierdlem81  46178  elaa2  46225  etransclem32  46257  sge0iunmptlemre  46406  voliunsge0lem  46463  meaiuninc3v  46475  isomenndlem  46521  ovnsubaddlem1  46561  hoidmvlelem1  46586  hoidmvlelem5  46590  smfaddlem1  46754  tworepnotupword  46877  2reu7  47105  2reu8  47106  f1oresf1o2  47285  mogoldbb  47779  2zrngagrp  48230  2zrngmmgm  48233