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

Theorem nfrab1 2856
Description: The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
nfrab1  |-  F/_ x { x  e.  A  |  ph }

Proof of Theorem nfrab1
StepHypRef Expression
1 df-rab 2683 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 nfab1 2550 . 2  |-  F/_ x { x  |  (
x  e.  A  /\  ph ) }
31, 2nfcxfr 2545 1  |-  F/_ x { x  e.  A  |  ph }
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1721   {cab 2398   F/_wnfc 2535   {crab 2678
This theorem is referenced by:  reusv2lem4  4694  reusv2  4696  reusv6OLD  4701  rabxfrd  4711  onminsb  4746  tfis  4801  riotaxfrd  6548  oawordeulem  6764  nnawordex  6847  rankidb  7690  tskwe  7801  cardmin2  7849  cardaleph  7934  cardmin  8403  nnwos  10508  neiptopnei  17159  imasnopn  17683  imasncld  17684  imasncls  17685  blval2  18566  iundisj  19403  mbfinf  19518  rabexgfGS  23948  rabss3d  23956  iundisjf  23990  iundisjfi  24113  esumpinfval  24424  hasheuni  24436  measvuni  24529  ballotlem7  24754  ballotth  24756  sltval2  25532  nobndlem5  25572  mbfposadd  26161  cover2  26313  rfcnpre1  27565  rfcnpre2  27577  dvcosre  27616  stoweidlem14  27638  stoweidlem26  27650  stoweidlem31  27655  stoweidlem34  27658  stoweidlem35  27659  stoweidlem46  27670  stoweidlem50  27674  stoweidlem51  27675  stoweidlem52  27676  stoweidlem53  27677  stoweidlem54  27678  stoweidlem57  27681  stoweidlem59  27683  bnj1230  28892  bnj1476  28936  bnj1204  29099  bnj1311  29111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683
  Copyright terms: Public domain W3C validator