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

Definition df-rab 2703
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 2698 . 2
52cv 1686 . . . . 5
65, 3wcel 1749 . . . 4
76, 1wa 362 . . 3
87, 2cab 2408 . 2
94, 8wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  rabid  2876  rabid2  2877  rabbi  2878  rabswap  2879  nfrab1  2880  nfrab  2881  rabbiia  2940  rabbidva2  2941  rabeqf  2944  cbvrab  2949  rabab  2969  elrabi  3092  elrabf  3093  elrab3t  3094  ralrab2  3103  rexrab2  3105  cbvrabcsf  3299  dfin5  3313  dfdif2  3314  ss2rab  3405  rabss  3406  ssrab  3407  rabss2  3412  ssrab2  3414  rabssab  3416  notab  3597  unrab  3598  inrab  3599  inrab2  3600  difrab  3601  dfrab3  3602  notrab  3604  rabun2  3606  dfnul3  3617  rabn0  3634  rab0  3635  dfif6  3771  rabsn  3919  reusn  3923  rabsneu  3925  elunirab  4078  elintrab  4115  ssintrab  4126  iunrab  4192  iinrab  4207  intexrab  4423  rmorabex  4524  exss  4527  rabxp  4846  mptpreima  5303  fndmin  5780  fncnvima2  5795  riotauni  6027  riotacl2  6035  snriota  6051  orduniss2  6414  exse2  6487  zfrep6  6514  xp2  6580  unielxp  6581  dfopab2  6597  suppvalbr  6663  ressuppss  6675  extmptsuppeq  6679  rankval3b  7980  scottexs  8041  scott0s  8042  kardex  8048  cardval2  8108  r0weon  8126  dfac2a  8246  axdc2lem  8564  sstskm  8955  nnzrab  10619  nn0zrab  10620  hashbclem  12146  wrdlenfi  12199  cshwsexa  12399  shftlem  12498  shftuz  12499  shftdm  12501  hashbc0  14006  cshwsiun  14066  submacs  15432  cycsubg  15646  eqglact  15669  dfrhm2  16631  aspval2  17225  psrbaglefi  17257  znunithash  17705  clsval2  18358  xkoptsub  18931  ptcmplem2  19329  cnblcld  20054  cncmet  20533  shft2rab  20691  sca2rab  20695  vmappw  22195  isusgra0  22954  nbgraf1olem5  23033  nb3graprlem1  23038  vdgrun  23250  vdgrfiun  23251  h2hcau  24060  dfch2  24489  hhcno  24987  hhcnf  24988  pjhmopidm  25266  elpjrn  25273  rabrab  25564  rabid2f  25565  rabfmpunirn  25648  mptctf  25701  maprnin  25711  fpwrelmapffslem  25712  fpwrelmap  25713  sigaex  26261  sigaval  26262  isrnsigaOLD  26264  ballotlem2  26574  setlikespec  27350  rabiun  28083  ptrest  28096  cnambfre  28111  areacirclem5  28159  neibastop3  28254  ispridlc  28541  eq0rabdioph  28788  rexrabdioph  28805  eldioph4b  28823  aomclem4  29083  rabexgf  29419  rabasiun  29904  wwlknprop  29994  wwlkextwrd  30034  wwlknfi  30044  wlknwwlknvbij  30046  clwwlkvbij  30137  wrdnval  30148  eclclwwlkn1  30180  rusgranumwlkl1  30233  rusgranumwlklem3  30243  rusgranumwlkb0  30245  rusgra0edg  30247  numclwwlkovf2  30351  rabsnif  30390  rabeqsn  30391  rabsssn  30392  bnj1441  31412  bnj110  31429  bj-rababwv  31851  bj-rabbida2  31871  bj-inrab  31880  lkrval2  32172  lfl1dim  32203  glbconxN  32459  dva1dim  34066  dib1dim2  34250  diclspsn  34276  dih1dimatlem  34411  dihglb2  34424  mapdvalc  34711  mapdval4N  34714  hdmapoc  35016
  Copyright terms: Public domain W3C validator