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

Theorem nfrab1 3429
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 3411 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 nfab1 2910 . 2 𝑥{𝑥 ∣ (𝑥𝐴𝜑)}
31, 2nfcxfr 2906 1 𝑥{𝑥𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 397  wcel 2107  {cab 2714  wnfc 2888  {crab 3410
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-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-rab 3411
This theorem is referenced by:  rabss3d  4044  reusv2lem4  5361  reusv2  5363  rabxfrd  5377  riotaxfrd  7353  onminsb  7734  tfis  7796  oawordeulem  8506  nnawordex  8589  rankidb  9743  tskwe  9893  cardmin2  9942  cardaleph  10032  cardmin  10507  nnwos  12847  neiptopnei  22499  dissnlocfin  22896  imasnopn  23057  imasncld  23058  imasncls  23059  blval2  23934  iundisj  24928  mbfinf  25045  sltval2  27020  lfgrnloop  28118  difrab2  31468  rabexgfGS  31469  eqrrabd  31472  iundisjf  31549  fimarab  31601  aciunf1  31621  fpwrelmap  31692  fpwrelmapffs  31693  iundisjfi  31741  locfinreflem  32461  zarcls  32495  ordtconnlem1  32545  esumrnmpt2  32707  esumpinfval  32712  hasheuni  32724  ldsysgenld  32799  measvuni  32853  eulerpartlemn  33021  ballotlem7  33175  ballotth  33177  reprdifc  33280  bnj1230  33454  bnj1476  33499  bnj1204  33664  bnj1311  33676  satfv1  33997  bj-rabtrALT  35430  topdifinfindis  35846  icorempo  35851  isbasisrelowllem1  35855  isbasisrelowllem2  35856  relowlssretop  35863  phpreu  36091  poimirlem26  36133  poimirlem27  36134  mbfposadd  36154  cover2  36202  naddwordnexlem4  41747  rababg  41920  rfcnpre1  43298  rfcnpre2  43310  ssrab2f  43401  infnsuprnmpt  43552  allbutfiinf  43729  supminfxr2  43778  pimxrneun  43798  fsumiunss  43890  limcperiod  43943  fnlimcnv  43982  fnlimfvre2  43992  fnlimf  43993  limsupequzmpt2  44033  liminfequzmpt2  44106  dvcosre  44227  stoweidlem14  44329  stoweidlem26  44341  stoweidlem31  44346  stoweidlem34  44349  stoweidlem35  44350  stoweidlem46  44361  stoweidlem50  44365  stoweidlem51  44366  stoweidlem52  44367  stoweidlem53  44368  stoweidlem54  44369  stoweidlem57  44372  stoweidlem59  44374  fourierdlem20  44442  fourierdlem31  44453  fourierdlem79  44500  sge0iunmptlemre  44730  ovnlerp  44877  opnvonmbllem1  44947  preimagelt  45014  preimalegt  45015  pimconstlt1  45017  pimltpnff  45018  pimrecltpos  45023  pimiooltgt  45025  pimdecfgtioc  45030  pimincfltioc  45031  pimdecfgtioo  45032  pimincfltioo  45033  preimageiingt  45035  preimaleiinlt  45036  pimgtmnff  45037  pimrecltneg  45039  sssmf  45053  incsmflem  45056  issmfle  45060  issmfgt  45071  smfaddlem1  45078  decsmflem  45081  issmfge  45085  smflimlem2  45087  smflim  45092  smfresal  45103  smfmullem2  45107  smfmullem4  45109  smfpimbor1lem2  45114  smflim2  45121  smfpimcclem  45122  smfsup  45129  smfinf  45133  smflimsuplem2  45136  smflimsuplem5  45139  smflimsuplem7  45141  smflimsup  45143  smfliminf  45146  smfdivdmmbl2  45156  fsupdm  45157  fsupdm2  45158  finfdm  45161  finfdm2  45162  prmdvdsfmtnof1lem1  45850
  Copyright terms: Public domain W3C validator