MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrab1 Unicode version

Theorem nfrab1 3038
Description: The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
nfrab1

Proof of Theorem nfrab1
StepHypRef Expression
1 df-rab 2816 . 2
2 nfab1 2621 . 2
31, 2nfcxfr 2617 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  e.wcel 1818  {cab 2442  F/_wnfc 2605  {crab 2811
This theorem is referenced by:  reusv2lem4  4656  reusv2  4658  reusv6OLD  4663  rabxfrd  4673  riotaxfrd  6288  onminsb  6634  tfis  6689  oawordeulem  7222  nnawordex  7305  rankidb  8239  tskwe  8352  cardmin2  8400  cardaleph  8491  cardmin  8960  nnwos  11178  neiptopnei  19633  dissnlocfin  20030  imasnopn  20191  imasncld  20192  imasncls  20193  blval2  21078  iundisj  21958  mbfinf  22072  rabexgfGS  27401  rabss3d  27412  iundisjf  27448  fimarab  27483  fpwrelmap  27556  fpwrelmapffs  27557  iundisjfi  27601  locfinreflem  27843  ordtconlem1  27906  esumpinfval  28079  hasheuni  28091  measvuni  28185  eulerpartlemn  28320  ballotlem7  28474  ballotth  28476  sltval2  29416  nobndlem5  29456  mbfposadd  30062  dvtanlem  30064  cover2  30204  rfcnpre1  31394  rfcnpre2  31406  limcperiod  31634  dvcosre  31706  stoweidlem14  31796  stoweidlem26  31808  stoweidlem31  31813  stoweidlem34  31816  stoweidlem35  31817  stoweidlem46  31828  stoweidlem50  31832  stoweidlem51  31833  stoweidlem52  31834  stoweidlem53  31835  stoweidlem54  31836  stoweidlem57  31839  stoweidlem59  31841  fourierdlem20  31909  fourierdlem31  31920  fourierdlem79  31968  bnj1230  33861  bnj1476  33905  bnj1204  34068  bnj1311  34080  bj-rabtrALT  34498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816
  Copyright terms: Public domain W3C validator