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

Theorem nfre1 3268
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 3115 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
2 nfe1 2152 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1854 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wa 399  wex 1781  wnf 1785  wcel 2112  wrex 3110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2143
This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786  df-rex 3115
This theorem is referenced by:  2rmorex  3696  2reurex  3701  reuan  3828  2reu4lem  4426  nfiu1  4918  reusv2lem3  5269  fvelimad  6711  fsnex  7021  eusvobj2  7132  fiun  7630  f1iun  7631  zfregcl  9046  scott0  9303  ac6c4  9896  lbzbi  12328  mreiincl  16863  lss1d  19732  neiptopnei  21741  neitr  21789  utopsnneiplem  22857  cfilucfil  23170  2sqmo  26025  mptelee  26693  isch3  29028  atom1d  30140  opreu2reuALT  30251  iinabrex  30336  xrofsup  30522  locfinreflem  31197  esumc  31424  esumrnmpt2  31441  hasheuni  31458  esumcvg  31459  esumcvgre  31464  voliune  31602  volfiniune  31603  ddemeas  31609  eulerpartlemgvv  31748  bnj900  32315  bnj1189  32395  bnj1204  32398  bnj1398  32420  bnj1444  32429  bnj1445  32430  bnj1446  32431  bnj1447  32432  bnj1467  32440  bnj1518  32450  bnj1519  32451  nosupbnd2  33330  iooelexlt  34780  fvineqsneq  34830  ptrest  35055  poimirlem26  35082  indexa  35170  filbcmb  35177  sdclem1  35180  heibor1  35247  dihglblem5  38593  suprnmpt  41791  disjinfi  41813  upbdrech  41930  ssfiunibd  41934  infxrunb2  41993  supxrunb3  42029  iccshift  42148  iooshift  42152  islpcn  42274  limsupre  42276  limclner  42286  limsupre3uzlem  42370  climuzlem  42378  xlimmnfv  42469  xlimpnfv  42473  itgperiod  42616  stoweidlem53  42688  stoweidlem57  42692  fourierdlem48  42789  fourierdlem51  42792  fourierdlem73  42814  fourierdlem81  42822  elaa2  42869  etransclem32  42901  sge0iunmptlemre  43047  voliunsge0lem  43104  meaiuninc3v  43116  isomenndlem  43162  ovnsubaddlem1  43202  hoidmvlelem1  43227  hoidmvlelem5  43231  smfaddlem1  43389  2reu7  43660  2reu8  43661  f1oresf1o2  43840  mogoldbb  44296  2zrngagrp  44560  2zrngmmgm  44563
  Copyright terms: Public domain W3C validator