MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfre1 Structured version   Visualization version   GIF version

Theorem nfre1 2987
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
StepHypRef Expression
1 df-rex 2901 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
2 nfe1 2013 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1770 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wa 382  wex 1694  wnf 1698  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-10 2005
This theorem depends on definitions:  df-bi 195  df-ex 1695  df-nf 1700  df-rex 2901
This theorem is referenced by:  r19.29an  3058  2rmorex  3378  nfiu1  4480  reusv2lem3  4792  elsnxpOLD  5581  fsnex  6416  eusvobj2  6520  fun11iun  6997  zfregcl  8360  zfregclOLD  8362  scott0  8610  ac6c4  9164  lbzbi  11611  mreiincl  16028  lss1d  18733  neiptopnei  20694  neitr  20742  utopsnneiplem  21809  cfilucfil  22122  mptelee  25521  isch3  27316  atom1d  28430  xrofsup  28757  2sqmo  28814  locfinreflem  29069  esumc  29274  esumrnmpt2  29291  hasheuni  29308  esumcvg  29309  esumcvgre  29314  voliune  29453  volfiniune  29454  ddemeas  29460  eulerpartlemgvv  29599  bnj900  30087  bnj1189  30165  bnj1204  30168  bnj1398  30190  bnj1444  30199  bnj1445  30200  bnj1446  30201  bnj1447  30202  bnj1467  30210  bnj1518  30220  bnj1519  30221  iooelexlt  32210  ptrest  32402  poimirlem26  32429  indexa  32522  filbcmb  32529  sdclem1  32533  heibor1  32603  dihglblem5  35429  suprnmpt  38174  disjinfi  38199  upbdrech  38284  ssfiunibd  38288  infxrunb2  38349  iccshift  38415  iooshift  38419  islpcn  38530  limsupre  38532  limclner  38542  itgperiod  38697  stoweidlem53  38770  stoweidlem57  38774  fourierdlem48  38871  fourierdlem51  38874  fourierdlem73  38896  fourierdlem81  38904  elaa2  38951  etransclem32  38983  sge0iunmptlemre  39132  voliunsge0lem  39189  isomenndlem  39244  ovnsubaddlem1  39284  hoidmvlelem1  39309  hoidmvlelem5  39313  smfaddlem1  39473  reuan  39653  2reurex  39654  2reu4a  39662  2reu7  39664  2reu8  39665  2zrngagrp  41755  2zrngmmgm  41758
  Copyright terms: Public domain W3C validator