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

Theorem nfrab1 3095
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 2901 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 nfab1 2749 . 2 𝑥{𝑥 ∣ (𝑥𝐴𝜑)}
31, 2nfcxfr 2745 1 𝑥{𝑥𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 382  wcel 1976  {cab 2592  wnfc 2734  {crab 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901
This theorem is referenced by:  reusv2lem4  4790  reusv2  4792  rabxfrd  4807  riotaxfrd  6516  onminsb  6865  tfis  6920  oawordeulem  7495  nnawordex  7578  rankidb  8520  tskwe  8633  cardmin2  8681  cardaleph  8769  cardmin  9239  nnwos  11584  neiptopnei  20685  dissnlocfin  21081  imasnopn  21242  imasncld  21243  imasncls  21244  blval2  22115  iundisj  23037  mbfinf  23152  rabexgfGS  28528  rabss3d  28539  iundisjf  28587  fimarab  28628  aciunf1  28648  fpwrelmap  28699  fpwrelmapffs  28700  iundisjfi  28745  locfinreflem  29038  ordtconlem1  29101  esumrnmpt2  29260  esumpinfval  29265  hasheuni  29277  ldsysgenld  29353  measvuni  29407  eulerpartlemn  29573  ballotlem7  29727  ballotth  29729  bnj1230  29930  bnj1476  29974  bnj1204  30137  bnj1311  30149  sltval2  30856  nobndlem5  30898  bj-rabtrALT  31919  topdifinfindis  32170  icorempt2  32175  isbasisrelowllem1  32179  isbasisrelowllem2  32180  relowlssretop  32187  phpreu  32363  poimirlem26  32405  poimirlem27  32406  mbfposadd  32427  cover2  32478  rababg  36698  rfcnpre1  38001  rfcnpre2  38013  ssrab2f  38131  fsumiunss  38443  limcperiod  38496  fnlimcnv  38535  fnlimfvre2  38545  fnlimf  38546  dvcosre  38600  stoweidlem14  38708  stoweidlem26  38720  stoweidlem31  38725  stoweidlem34  38728  stoweidlem35  38729  stoweidlem46  38740  stoweidlem50  38744  stoweidlem51  38745  stoweidlem52  38746  stoweidlem53  38747  stoweidlem54  38748  stoweidlem57  38751  stoweidlem59  38753  fourierdlem20  38821  fourierdlem31  38832  fourierdlem79  38879  sge0iunmptlemre  39109  ovnlerp  39253  opnvonmbllem1  39323  preimagelt  39390  preimalegt  39391  pimconstlt1  39393  pimltpnf  39394  pimrecltpos  39397  pimiooltgt  39399  pimdecfgtioc  39403  pimincfltioc  39404  pimdecfgtioo  39405  pimincfltioo  39406  preimageiingt  39408  preimaleiinlt  39409  pimrecltneg  39411  sssmf  39426  incsmflem  39429  issmfle  39433  issmfgt  39444  smfaddlem1  39450  decsmflem  39453  issmfge  39457  smflimlem2  39459  smflim  39464  smfresal  39474  smfmullem2  39478  smfmullem4  39480  smfpimbor1lem2  39485  prmdvdsfmtnof1lem1  39836  lfgrnloop  40349
  Copyright terms: Public domain W3C validator