Theorem nfre1 3262

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  3725  2reurex  3731  reuan  3859  2reu4lem  4485  nfiu1  4991  nfiu1OLD  4992  reusv2lem3  5355  fvelimad  6928  fsnex  7258  eusvobj2  7379  fiun  7921  f1iun  7922  zfregcl  9547  scott0  9839  ac6c4  10434  lbzbi  12895  mreiincl  17557  lss1d  20869  neiptopnei  23019  neitr  23067  utopsnneiplem  24135  cfilucfil  24447  2sqmo  27348  nosupbnd2  27628  noinfbnd2  27643  mptelee  28822  isch3  31170  atom1d  32282  opreu2reuALT  32406  iinabrex  32498  xrofsup  32690  locfinreflem  33830  esumc  34041  esumrnmpt2  34058  hasheuni  34075  esumcvg  34076  esumcvgre  34081  voliune  34219  volfiniune  34220  ddemeas  34226  eulerpartlemgvv  34367  bnj900  34919  bnj1189  34999  bnj1204  35002  bnj1398  35024  bnj1444  35033  bnj1445  35034  bnj1446  35035  bnj1447  35036  bnj1467  35044  bnj1518  35054  bnj1519  35055  iooelexlt  37350  fvineqsneq  37400  ptrest  37613  poimirlem26  37640  indexa  37727  filbcmb  37734  sdclem1  37737  heibor1  37804  dihglblem5  41292  unielss  43207  oaun3lem1  43363  suprnmpt  45168  disjinfi  45186  upbdrech  45303  ssfiunibd  45307  infxrunb2  45364  supxrunb3  45395  iccshift  45516  iooshift  45520  islpcn  45637  limsupre  45639  limclner  45649  limsupre3uzlem  45733  climuzlem  45741  xlimmnfv  45832  xlimpnfv  45836  itgperiod  45979  stoweidlem53  46051  stoweidlem57  46055  fourierdlem48  46152  fourierdlem51  46155  fourierdlem73  46177  fourierdlem81  46185  elaa2  46232  etransclem32  46264  sge0iunmptlemre  46413  voliunsge0lem  46470  meaiuninc3v  46482  isomenndlem  46528  ovnsubaddlem1  46568  hoidmvlelem1  46593  hoidmvlelem5  46597  smfaddlem1  46761  tworepnotupword  46884  2reu7  47112  2reu8  47113  f1oresf1o2  47292  mogoldbb  47786  2zrngagrp  48237  2zrngmmgm  48240