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

Theorem nfre1 3267
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 3071 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
2 nfe1 2148 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1856 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wa 397  wex 1782  wnf 1786  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2138
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-rex 3071
This theorem is referenced by:  2rmorex  3713  2reurex  3719  reuan  3853  2reu4lem  4484  nfiu1  4989  reusv2lem3  5356  fvelimad  6910  fsnex  7230  eusvobj2  7350  fiun  7876  f1iun  7877  zfregcl  9535  scott0  9827  ac6c4  10422  lbzbi  12866  mreiincl  17481  lss1d  20439  neiptopnei  22499  neitr  22547  utopsnneiplem  23615  cfilucfil  23931  2sqmo  26801  nosupbnd2  27080  noinfbnd2  27095  mptelee  27886  isch3  30225  atom1d  31337  opreu2reuALT  31448  iinabrex  31533  xrofsup  31719  locfinreflem  32478  esumc  32707  esumrnmpt2  32724  hasheuni  32741  esumcvg  32742  esumcvgre  32747  voliune  32885  volfiniune  32886  ddemeas  32892  eulerpartlemgvv  33033  bnj900  33598  bnj1189  33678  bnj1204  33681  bnj1398  33703  bnj1444  33712  bnj1445  33713  bnj1446  33714  bnj1447  33715  bnj1467  33723  bnj1518  33733  bnj1519  33734  iooelexlt  35879  fvineqsneq  35929  ptrest  36123  poimirlem26  36150  indexa  36238  filbcmb  36245  sdclem1  36248  heibor1  36315  dihglblem5  39807  unielss  41595  oaun3lem1  41733  suprnmpt  43479  disjinfi  43500  upbdrech  43626  ssfiunibd  43630  infxrunb2  43689  supxrunb3  43720  iccshift  43842  iooshift  43846  islpcn  43966  limsupre  43968  limclner  43978  limsupre3uzlem  44062  climuzlem  44070  xlimmnfv  44161  xlimpnfv  44165  itgperiod  44308  stoweidlem53  44380  stoweidlem57  44384  fourierdlem48  44481  fourierdlem51  44484  fourierdlem73  44506  fourierdlem81  44514  elaa2  44561  etransclem32  44593  sge0iunmptlemre  44742  voliunsge0lem  44799  meaiuninc3v  44811  isomenndlem  44857  ovnsubaddlem1  44897  hoidmvlelem1  44922  hoidmvlelem5  44926  smfaddlem1  45090  tworepnotupword  45211  2reu7  45429  2reu8  45430  f1oresf1o2  45609  mogoldbb  46063  2zrngagrp  46327  2zrngmmgm  46330
  Copyright terms: Public domain W3C validator