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

Definition df-rab 2917
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 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3crab 2912 . 2 class {𝑥𝐴𝜑}
52cv 1479 . . . . 5 class 𝑥
65, 3wcel 1987 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2607 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1480 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3110  rabid2  3111  rabid2f  3112  rabbi  3113  rabswap  3114  nfrab1  3115  nfrab  3116  rabbiia  3177  rabbidva2  3178  rabeqf  3182  cbvrab  3188  rabab  3213  elrabi  3347  elrabf  3348  elrab3t  3350  ralrab2  3359  rexrab2  3361  cbvrabcsf  3554  dfin5  3568  dfdif2  3569  ss2rab  3663  rabss  3664  ssrab  3665  rabss2  3670  ssrab2  3672  rabssab  3674  notab  3879  unrab  3880  inrab  3881  inrab2  3882  difrab  3883  dfrab3  3884  notrab  3886  rabun2  3888  dfnul3  3900  rab0  3935  rab0OLD  3936  rabeq0  3937  rabn0OLD  3939  dfif6  4067  rabeqsn  4192  rabsssn  4193  rabsn  4233  rabsnifsb  4234  reusn  4239  rabsneu  4241  elunirab  4421  elintrab  4460  ssintrab  4472  rabasiun  4496  iunrab  4540  iinrab  4555  intexrab  4793  rmorabex  4899  exss  4902  rabxp  5124  mptpreima  5597  setlikespec  5670  fndmin  6290  fncnvima2  6305  riotauni  6582  riotacl2  6589  snriota  6606  orduniss2  6995  exse2  7067  zfrep6  7096  xp2  7163  unielxp  7164  dfopab2  7182  suppvalbr  7259  ressuppss  7274  rankval3b  8649  scottexs  8710  scott0s  8711  kardex  8717  cardval2  8777  r0weon  8795  axdc2lem  9230  sstskm  9624  negfi  10931  nnzrab  11365  nn0zrab  11366  prprrab  13209  wrdnval  13290  cshwsexa  13523  shftlem  13758  shftuz  13759  shftdm  13761  hashbc0  15652  cshwsiun  15749  submacs  17305  cycsubg  17562  eqglact  17585  dfrhm2  18657  aspval2  19287  psrbaglefi  19312  znunithash  19853  clsval2  20794  xkoptsub  21397  ptcmplem2  21797  cnblcld  22518  cncmet  23059  shft2rab  23216  sca2rab  23220  vmappw  24776  2lgslem1b  25051  nb3grprlem1  26203  vtxdun  26297  rusgrprc  26390  ewlksfval  26401  wwlksnfi  26704  wlksnwwlknvbij  26706  rusgrnumwwlkb0  26767  clwwlksvbij  26822  eclclwwlksn1  26852  h2hcau  27724  dfch2  28154  hhcno  28651  hhcnf  28652  pjhmopidm  28930  elpjrn  28937  rabrab  29227  rabfmpunirn  29336  mptctf  29379  maprnin  29390  fpwrelmapffslem  29391  fpwrelmap  29392  sigaex  29995  sigaval  29996  isrnsigaOLD  29998  ballotlem2  30373  bnj1441  30672  bnj110  30689  neibastop3  32052  bj-rababwv  32567  bj-rabbida2  32613  bj-inrab  32623  rabiun  33053  ptrest  33079  poimirlem26  33106  poimirlem27  33107  cnambfre  33129  areacirclem5  33175  ispridlc  33540  lkrval2  33896  lfl1dim  33927  glbconxN  34183  dva1dim  35792  dib1dim2  35976  diclspsn  36002  dih1dimatlem  36137  dihglb2  36150  hdmapoc  36742  eq0rabdioph  36859  rexrabdioph  36877  eldioph4b  36894  aomclem4  37146  clcnvlem  37450  ntrneiel2  37905  rabexgf  38705  ssrabf  38822  rabssf  38827  rabbida2  38842  rabbida3  38845  sprvalpw  41048  submgmacs  41122
  Copyright terms: Public domain W3C validator