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

Definition df-rab 2809
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 2804 . 2
52cv 1369 . . . . 5
65, 3wcel 1758 . . . 4
76, 1wa 369 . . 3
87, 2cab 2439 . 2
94, 8wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3006  rabid2  3007  rabbi  3008  rabswap  3009  nfrab1  3010  nfrab  3011  rabbiia  3070  rabbidva2  3071  rabeqf  3074  cbvrab  3079  rabab  3099  elrabi  3224  elrabf  3225  elrab3t  3226  ralrab2  3235  rexrab2  3237  cbvrabcsf  3436  dfin5  3450  dfdif2  3451  ss2rab  3542  rabss  3543  ssrab  3544  rabss2  3549  ssrab2  3551  rabssab  3553  notab  3734  unrab  3735  inrab  3736  inrab2  3737  difrab  3738  dfrab3  3739  notrab  3741  rabun2  3743  dfnul3  3754  rabn0  3771  rab0  3772  dfif6  3908  rabsn  4059  rabsnifsb  4060  reusn  4065  rabsneu  4067  elunirab  4220  elintrab  4257  ssintrab  4268  iunrab  4334  iinrab  4349  intexrab  4568  rmorabex  4669  exss  4672  rabxp  4992  mptpreima  5450  fndmin  5933  fncnvima2  5948  riotauni  6189  riotacl2  6197  snriota  6213  orduniss2  6577  exse2  6650  zfrep6  6678  xp2  6744  unielxp  6745  dfopab2  6761  suppvalbr  6828  ressuppss  6842  extmptsuppeq  6847  rankval3b  8170  scottexs  8231  scott0s  8232  kardex  8238  cardval2  8298  r0weon  8316  dfac2a  8436  axdc2lem  8754  sstskm  9146  nnzrab  10812  nn0zrab  10813  hashbclem  12363  wrdlenfi  12416  cshwsexa  12616  shftlem  12715  shftuz  12716  shftdm  12718  hashbc0  14224  cshwsiun  14284  submacs  15652  cycsubg  15868  eqglact  15891  dfrhm2  16984  aspval2  17593  psrbaglefi  17617  psrbaglefiOLD  17618  znunithash  18190  clsval2  19053  xkoptsub  19626  ptcmplem2  20024  cnblcld  20753  cncmet  21232  shft2rab  21390  sca2rab  21394  vmappw  22854  isusgra0  23744  nbgraf1olem5  23823  nb3graprlem1  23828  vdgrun  24040  vdgrfiun  24041  h2hcau  24850  dfch2  25279  hhcno  25777  hhcnf  25778  pjhmopidm  26056  elpjrn  26063  rabrab  26353  rabid2f  26354  rabfmpunirn  26435  mptctf  26488  maprnin  26498  fpwrelmapffslem  26499  fpwrelmap  26500  sigaex  27009  sigaval  27010  isrnsigaOLD  27012  ballotlem2  27327  setlikespec  28104  rabiun  28872  ptrest  28885  cnambfre  28900  areacirclem5  28948  neibastop3  29043  ispridlc  29330  eq0rabdioph  29575  rexrabdioph  29592  eldioph4b  29610  aomclem4  29870  rabexgf  30206  rabasiun  31107  wwlknprop  31197  wwlkextwrd  31237  wwlknfi  31247  wlknwwlknvbij  31249  clwwlkvbij  31340  wrdnval  31351  eclclwwlkn1  31383  rusgranumwlkl1  31436  rusgranumwlklem3  31446  rusgranumwlkb0  31448  rusgra0edg  31450  numclwwlkovf2  31554  rabeqsn  31594  rabsssn  31595  bnj1441  32677  bnj110  32694  bj-rababwv  33223  bj-rabbida2  33265  bj-inrab  33275  lkrval2  33586  lfl1dim  33617  glbconxN  33873  dva1dim  35480  dib1dim2  35664  diclspsn  35690  dih1dimatlem  35825  dihglb2  35838  mapdvalc  36125  mapdval4N  36128  hdmapoc  36430
  Copyright terms: Public domain W3C validator