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

Definition df-rab 2721
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 2716 . 2
52cv 1653 . . . . 5
65, 3wcel 1728 . . . 4
76, 1wa 360 . . 3
87, 2cab 2429 . 2
94, 8wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  rabid  2891  rabid2  2892  rabbi  2893  rabswap  2894  nfrab1  2895  nfrab  2896  rabbiia  2955  rabeqf  2958  cbvrab  2963  rabab  2982  elrabi  3099  elrabf  3100  ralrab2  3109  rexrab2  3111  cbvrabcsf  3303  dfin5  3317  dfdif2  3318  ss2rab  3408  rabss  3409  ssrab  3410  rabss2  3415  ssrab2  3417  rabssab  3419  notab  3599  unrab  3600  inrab  3601  inrab2  3602  difrab  3603  dfrab2  3604  dfrab3  3605  notrab  3606  rabun2  3608  dfnul3  3619  rabn0  3635  rab0  3636  dfif6  3768  rabsn  3901  reusn  3905  rabsneu  3907  elunirab  4055  elintrab  4091  ssintrab  4102  iunrab  4168  iinrab  4183  intexrab  4398  rmorabex  4462  exss  4465  orduniss2  4854  rabxp  4954  exse2  5282  mptpreima  5409  fndmin  5885  fncnvima2  5900  zfrep6  6016  xp2  6434  unielxp  6435  dfopab2  6451  riotauni  6606  riotacl2  6613  snriota  6629  cantnfreslem  7680  rankval3b  7801  scottexs  7862  scott0s  7863  kardex  7869  cardval2  7929  r0weon  7945  dfac2a  8061  axdc2lem  8379  sstskm  8768  nnzrab  10360  nn0zrab  10361  hashbclem  11752  shftlem  11934  shftuz  11935  shftdm  11937  hashbc0  13424  submacs  14816  cycsubg  15019  eqglact  15042  dfrhm2  15872  aspval2  16456  psrbaglefi  16488  znunithash  16896  clsval2  17165  xkoptsub  17737  ptcmplem2  18135  cnblcld  18860  cncmet  19326  shft2rab  19455  sca2rab  19459  vmappw  20950  isusgra0  21427  nbgraf1olem5  21506  nb3graprlem1  21511  vdgrun  21723  vdgrfiun  21724  h2hcau  22533  dfch2  22960  hhcno  23458  hhcnf  23459  pjhmopidm  23737  elpjrn  23744  rabid2f  24016  rabbidva2  24035  rabfmpunirn  24113  mptctf  24160  sigaex  24541  sigaval  24542  isrnsigaOLD  24544  elrab3t  24716  rabrab  24734  maprnin  24735  fpwrelmapffslem  24736  fpwrelmap  24737  ballotlem2  24850  setlikespec  25566  rabiun  26340  cnambfre  26364  areacirclem5  26407  neibastop3  26502  ispridlc  26791  eq0rabdioph  27016  rexrabdioph  27033  eldioph4b  27051  aomclem4  27311  rabexgf  27849  cshwsiun  28484  cshwsexa  28489  wwlknprop  28532  bnj1441  29453  bnj110  29470  lkrval2  30128  lfl1dim  30159  glbconxN  30415  dva1dim  32022  dib1dim2  32206  diclspsn  32232  dih1dimatlem  32367  dihglb2  32380  mapdvalc  32667  mapdval4N  32670  hdmapoc  32972
  Copyright terms: Public domain W3C validator