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 2904
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 2899 . 2 class {𝑥𝐴𝜑}
52cv 1473 . . . . 5 class 𝑥
65, 3wcel 1976 . . . 4 wff 𝑥𝐴
76, 1wa 382 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2595 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1474 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3094  rabid2  3095  rabbi  3096  rabswap  3097  nfrab1  3098  nfrab  3099  rabbiia  3160  rabbidva2  3161  rabeqf  3164  cbvrab  3170  rabab  3195  elrabi  3327  elrabf  3328  elrab3t  3329  ralrab2  3338  rexrab2  3340  cbvrabcsf  3533  dfin5  3547  dfdif2  3548  ss2rab  3640  rabss  3641  ssrab  3642  rabss2  3647  ssrab2  3649  rabssab  3651  notab  3855  unrab  3856  inrab  3857  inrab2  3858  difrab  3859  dfrab3  3860  notrab  3862  rabun2  3864  dfnul3  3876  rab0  3908  rab0OLD  3909  rabeq0  3910  rabn0OLD  3912  dfif6  4038  rabeqsn  4160  rabsssn  4161  rabsn  4199  rabsnifsb  4200  reusn  4205  rabsneu  4207  elunirab  4378  elintrab  4417  ssintrab  4429  rabasiun  4453  iunrab  4497  iinrab  4512  intexrab  4744  rmorabex  4848  exss  4851  rabxp  5067  mptpreima  5530  setlikespec  5603  fndmin  6216  fncnvima2  6231  riotauni  6494  riotacl2  6501  snriota  6517  orduniss2  6902  exse2  6975  zfrep6  7004  xp2  7071  unielxp  7072  dfopab2  7090  suppvalbr  7163  ressuppss  7178  rankval3b  8549  scottexs  8610  scott0s  8611  kardex  8617  cardval2  8677  r0weon  8695  axdc2lem  9130  sstskm  9520  negfi  10822  nnzrab  11240  nn0zrab  11241  wrdnval  13138  cshwsexa  13369  shftlem  13604  shftuz  13605  shftdm  13607  hashbc0  15495  cshwsiun  15592  submacs  17136  cycsubg  17393  eqglact  17416  dfrhm2  18488  aspval2  19116  psrbaglefi  19141  znunithash  19679  clsval2  20611  xkoptsub  21214  ptcmplem2  21614  cnblcld  22335  cncmet  22871  shft2rab  23027  sca2rab  23031  vmappw  24586  2lgslem1b  24861  usgraop  25672  nbgraf1olem5  25767  nb3graprlem1  25773  wwlknprop  26007  wwlknfi  26059  wlknwwlknvbij  26061  clwwlkvbij  26122  eclclwwlkn1  26152  vdgrun  26221  vdgrfiun  26222  rusgranumwlkb0  26273  rusgra0edg  26275  h2hcau  27013  dfch2  27443  hhcno  27940  hhcnf  27941  pjhmopidm  28219  elpjrn  28226  rabrab  28515  rabid2f  28517  rabfmpunirn  28626  mptctf  28676  maprnin  28687  fpwrelmapffslem  28688  fpwrelmap  28689  sigaex  29292  sigaval  29293  isrnsigaOLD  29295  ballotlem2  29670  bnj1441  29958  bnj110  29975  neibastop3  31320  bj-rababwv  31844  bj-rabbida2  31888  bj-inrab  31898  rabiun  32335  ptrest  32361  poimirlem26  32388  poimirlem27  32389  cnambfre  32411  areacirclem5  32457  ispridlc  32822  lkrval2  33178  lfl1dim  33209  glbconxN  33465  dva1dim  35074  dib1dim2  35258  diclspsn  35284  dih1dimatlem  35419  dihglb2  35432  hdmapoc  36024  eq0rabdioph  36141  rexrabdioph  36159  eldioph4b  36176  aomclem4  36428  clcnvlem  36732  ntrneiel2  37187  rabexgf  37989  ssrabf  38112  rabssf  38117  prprrab  40176  nb3grprlem1  40589  vtxdun  40677  rusgrprc  40771  ewlksfval  40784  wwlksnfi  41093  wlksnwwlknvbij  41095  rusgrnumwwlkb0  41155  clwwlksvbij  41210  eclclwwlksn1  41240  submgmacs  41575
  Copyright terms: Public domain W3C validator