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

Definition df-rab 2768
Description: Define a restricted class abstraction (class builder), which is the class of all in such that is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-rab

Detailed syntax breakdown of Definition df-rab
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 cA . . 3
41, 2, 3crab 2763 . 2
52cv 1669 . . . . 5
65, 3wcel 1732 . . . 4
76, 1wa 360 . . 3
87, 2cab 2475 . 2
94, 8wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  rabid  2940  rabid2  2941  rabbi  2942  rabswap  2943  nfrab1  2944  nfrab  2945  rabbiia  3004  rabbidva2  3005  rabeqf  3008  cbvrab  3013  rabab  3032  elrabi  3152  elrabf  3153  elrab3t  3154  ralrab2  3163  rexrab2  3165  cbvrabcsf  3359  dfin5  3373  dfdif2  3374  ss2rab  3465  rabss  3466  ssrab  3467  rabss2  3472  ssrab2  3474  rabssab  3476  notab  3656  unrab  3657  inrab  3658  inrab2  3659  difrab  3660  dfrab2  3661  dfrab3  3662  notrab  3663  rabun2  3665  dfnul3  3676  rabn0  3692  rab0  3693  dfif6  3828  rabsn  3973  reusn  3977  rabsneu  3979  elunirab  4129  elintrab  4166  ssintrab  4177  iunrab  4243  iinrab  4258  intexrab  4474  rmorabex  4575  exss  4578  rabxp  4897  mptpreima  5351  fndmin  5826  fncnvima2  5841  riotauni  6069  riotacl2  6077  snriota  6093  orduniss2  6454  exse2  6526  zfrep6  6552  xp2  6617  unielxp  6618  dfopab2  6634  cantnfreslem  7798  rankval3b  7919  scottexs  7980  scott0s  7981  kardex  7987  cardval2  8047  r0weon  8065  dfac2a  8181  axdc2lem  8499  sstskm  8888  nnzrab  10538  nn0zrab  10539  hashbclem  12052  wrdlenfi  12105  cshwsexa  12305  shftlem  12404  shftuz  12405  shftdm  12407  hashbc0  13913  cshwsiun  13973  submacs  15332  cycsubg  15539  eqglact  15562  dfrhm2  16437  aspval2  17030  psrbaglefi  17062  znunithash  17470  clsval2  18128  xkoptsub  18701  ptcmplem2  19099  cnblcld  19824  cncmet  20290  shft2rab  20419  sca2rab  20423  vmappw  21920  isusgra0  22397  nbgraf1olem5  22476  nb3graprlem1  22481  vdgrun  22693  vdgrfiun  22694  h2hcau  23503  dfch2  23932  hhcno  24430  hhcnf  24431  pjhmopidm  24709  elpjrn  24716  rabrab  25012  rabid2f  25013  rabfmpunirn  25098  mptctf  25151  maprnin  25161  fpwrelmapffslem  25162  fpwrelmap  25163  sigaex  25732  sigaval  25733  isrnsigaOLD  25735  ballotlem2  26021  setlikespec  26801  rabiun  27596  cnambfre  27620  areacirclem5  27668  neibastop3  27763  ispridlc  28052  eq0rabdioph  28263  rexrabdioph  28280  eldioph4b  28298  aomclem4  28558  rabexgf  28921  rabasiun  29411  wwlknprop  29501  wwlkextwrd  29541  wwlknfi  29551  wlknwwlknvbij  29553  clwwlkvbij  29644  wrdnval  29655  eclclwwlkn1  29687  rusgranumwlkl1  29740  rusgranumwlklem3  29750  rusgranumwlkb0  29752  rusgra0edg  29754  numclwwlkovf2  29858  bnj1441  30682  bnj110  30699  lkrval2  31438  lfl1dim  31469  glbconxN  31725  dva1dim  33332  dib1dim2  33516  diclspsn  33542  dih1dimatlem  33677  dihglb2  33690  mapdvalc  33977  mapdval4N  33980  hdmapoc  34282
  Copyright terms: Public domain W3C validator