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

Theorem nfrab1 3152
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 2950 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 nfab1 2795 . 2 𝑥{𝑥 ∣ (𝑥𝐴𝜑)}
31, 2nfcxfr 2791 1 𝑥{𝑥𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 383  wcel 2030  {cab 2637  wnfc 2780  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950
This theorem is referenced by:  reusv2lem4  4902  reusv2  4904  rabxfrd  4919  riotaxfrd  6682  onminsb  7041  tfis  7096  oawordeulem  7679  nnawordex  7762  rankidb  8701  tskwe  8814  cardmin2  8862  cardaleph  8950  cardmin  9424  nnwos  11793  neiptopnei  20984  dissnlocfin  21380  imasnopn  21541  imasncld  21542  imasncls  21543  blval2  22414  iundisj  23362  mbfinf  23477  lfgrnloop  26065  extwwlkfab  27342  numclwlk1lem2  27350  difrab2  29465  rabexgfGS  29466  rabss3d  29477  iundisjf  29528  fimarab  29573  aciunf1  29591  fpwrelmap  29636  fpwrelmapffs  29637  iundisjfi  29683  locfinreflem  30035  ordtconnlem1  30098  esumrnmpt2  30258  esumpinfval  30263  hasheuni  30275  ldsysgenld  30351  measvuni  30405  eulerpartlemn  30571  ballotlem7  30725  ballotth  30727  reprdifc  30833  bnj1230  30999  bnj1476  31043  bnj1204  31206  bnj1311  31218  sltval2  31934  bj-rabtrALT  33052  topdifinfindis  33324  icorempt2  33329  isbasisrelowllem1  33333  isbasisrelowllem2  33334  relowlssretop  33341  phpreu  33523  poimirlem26  33565  poimirlem27  33566  mbfposadd  33587  cover2  33638  rababg  38196  rfcnpre1  39492  rfcnpre2  39504  ssrab2f  39614  infnsuprnmpt  39779  allbutfiinf  39960  supminfxr2  40012  fsumiunss  40125  limcperiod  40178  fnlimcnv  40217  fnlimfvre2  40227  fnlimf  40228  limsupequzmpt2  40268  liminfequzmpt2  40341  dvcosre  40444  stoweidlem14  40549  stoweidlem26  40561  stoweidlem31  40566  stoweidlem34  40569  stoweidlem35  40570  stoweidlem46  40581  stoweidlem50  40585  stoweidlem51  40586  stoweidlem52  40587  stoweidlem53  40588  stoweidlem54  40589  stoweidlem57  40592  stoweidlem59  40594  fourierdlem20  40662  fourierdlem31  40673  fourierdlem79  40720  sge0iunmptlemre  40950  ovnlerp  41097  opnvonmbllem1  41167  preimagelt  41233  preimalegt  41234  pimconstlt1  41236  pimltpnf  41237  pimrecltpos  41240  pimiooltgt  41242  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  preimageiingt  41251  preimaleiinlt  41252  pimrecltneg  41254  sssmf  41268  incsmflem  41271  issmfle  41275  issmfgt  41286  smfaddlem1  41292  decsmflem  41295  issmfge  41299  smflimlem2  41301  smflim  41306  smfresal  41316  smfmullem2  41320  smfmullem4  41322  smfpimbor1lem2  41327  smflim2  41333  smfpimcclem  41334  smfsup  41341  smfinf  41345  smflimsuplem2  41348  smflimsuplem3  41349  smflimsuplem5  41351  smflimsuplem7  41353  smflimsup  41355  smfliminf  41358  prmdvdsfmtnof1lem1  41821
  Copyright terms: Public domain W3C validator