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

Definition df-rab 2816
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 2811 . 2
52cv 1394 . . . . 5
65, 3wcel 1818 . . . 4
76, 1wa 369 . . 3
87, 2cab 2442 . 2
94, 8wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3034  rabid2  3035  rabbi  3036  rabswap  3037  nfrab1  3038  nfrab  3039  rabbiia  3098  rabbidva2  3099  rabeqf  3102  cbvrab  3107  rabab  3127  elrabi  3254  elrabf  3255  elrab3t  3256  ralrab2  3265  rexrab2  3267  cbvrabcsf  3469  dfin5  3483  dfdif2  3484  ss2rab  3575  rabss  3576  ssrab  3577  rabss2  3582  ssrab2  3584  rabssab  3586  notab  3767  unrab  3768  inrab  3769  inrab2  3770  difrab  3771  dfrab3  3772  notrab  3774  rabun2  3776  dfnul3  3787  rabn0  3805  rab0  3806  dfif6  3944  rabsn  4097  rabsnifsb  4098  reusn  4103  rabsneu  4105  elunirab  4261  elintrab  4298  ssintrab  4310  rabasiun  4334  iunrab  4377  iinrab  4392  intexrab  4611  rmorabex  4712  exss  4715  rabxp  5041  mptpreima  5505  fndmin  5994  fncnvima2  6009  riotauni  6263  riotacl2  6271  snriota  6287  orduniss2  6668  exse2  6739  zfrep6  6768  xp2  6835  unielxp  6836  dfopab2  6854  suppvalbr  6922  ressuppss  6938  rankval3b  8265  scottexs  8326  scott0s  8327  kardex  8333  cardval2  8393  r0weon  8411  axdc2lem  8849  sstskm  9241  nnzrab  10917  nn0zrab  10918  wrdnval  12571  cshwsexa  12792  shftlem  12901  shftuz  12902  shftdm  12904  hashbc0  14523  cshwsiun  14584  submacs  15996  cycsubg  16229  eqglact  16252  dfrhm2  17366  aspval2  17996  psrbaglefi  18023  psrbaglefiOLD  18024  znunithash  18603  clsval2  19551  xkoptsub  20155  ptcmplem2  20553  cnblcld  21282  cncmet  21761  shft2rab  21919  sca2rab  21923  vmappw  23390  usgraop  24350  nbgraf1olem5  24445  nb3graprlem1  24451  wwlknprop  24686  wwlknfi  24738  wlknwwlknvbij  24740  clwwlkvbij  24801  eclclwwlkn1  24832  vdgrun  24901  vdgrfiun  24902  rusgranumwlkb0  24953  rusgra0edg  24955  h2hcau  25896  dfch2  26325  hhcno  26823  hhcnf  26824  pjhmopidm  27102  elpjrn  27109  rabrab  27399  rabid2f  27400  rabfmpunirn  27491  mptctf  27544  maprnin  27554  fpwrelmapffslem  27555  fpwrelmap  27556  sigaex  28109  sigaval  28110  isrnsigaOLD  28112  ballotlem2  28427  setlikespec  29267  rabiun  30036  ptrest  30048  cnambfre  30063  areacirclem5  30111  neibastop3  30180  ispridlc  30467  eq0rabdioph  30710  rexrabdioph  30727  eldioph4b  30745  aomclem4  31003  rabexgf  31399  submgmacs  32492  rabeqsn  32919  rabsssn  32920  bnj1441  33899  bnj110  33916  bj-rababwv  34443  bj-rabbida2  34485  bj-inrab  34495  lkrval2  34815  lfl1dim  34846  glbconxN  35102  dva1dim  36711  dib1dim2  36895  diclspsn  36921  dih1dimatlem  37056  dihglb2  37069  hdmapoc  37661
  Copyright terms: Public domain W3C validator