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 2905
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 2900 . 2 class {𝑥𝐴𝜑}
52cv 1474 . . . . 5 class 𝑥
65, 3wcel 1977 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2596 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1475 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3095  rabid2  3096  rabbi  3097  rabswap  3098  nfrab1  3099  nfrab  3100  rabbiia  3161  rabbidva2  3162  rabeqf  3165  cbvrab  3171  rabab  3196  elrabi  3328  elrabf  3329  elrab3t  3330  ralrab2  3339  rexrab2  3341  cbvrabcsf  3534  dfin5  3548  dfdif2  3549  ss2rab  3641  rabss  3642  ssrab  3643  rabss2  3648  ssrab2  3650  rabssab  3652  notab  3856  unrab  3857  inrab  3858  inrab2  3859  difrab  3860  dfrab3  3861  notrab  3863  rabun2  3865  dfnul3  3877  rab0  3909  rab0OLD  3910  rabeq0  3911  rabn0OLD  3913  dfif6  4039  rabeqsn  4161  rabsssn  4162  rabsn  4200  rabsnifsb  4201  reusn  4206  rabsneu  4208  elunirab  4384  elintrab  4423  ssintrab  4435  rabasiun  4459  iunrab  4503  iinrab  4518  intexrab  4750  rmorabex  4855  exss  4858  rabxp  5078  mptpreima  5545  setlikespec  5618  fndmin  6232  fncnvima2  6247  riotauni  6517  riotacl2  6524  snriota  6540  orduniss2  6925  exse2  6998  zfrep6  7027  xp2  7094  unielxp  7095  dfopab2  7113  suppvalbr  7186  ressuppss  7201  rankval3b  8572  scottexs  8633  scott0s  8634  kardex  8640  cardval2  8700  r0weon  8718  axdc2lem  9153  sstskm  9543  negfi  10850  nnzrab  11282  nn0zrab  11283  prprrab  13112  wrdnval  13190  cshwsexa  13421  shftlem  13656  shftuz  13657  shftdm  13659  hashbc0  15547  cshwsiun  15644  submacs  17188  cycsubg  17445  eqglact  17468  dfrhm2  18540  aspval2  19168  psrbaglefi  19193  znunithash  19732  clsval2  20664  xkoptsub  21267  ptcmplem2  21667  cnblcld  22388  cncmet  22927  shft2rab  23083  sca2rab  23087  vmappw  24642  2lgslem1b  24917  usgraop  25879  nbgraf1olem5  25974  nb3graprlem1  25980  wwlknprop  26214  wwlknfi  26266  wlknwwlknvbij  26268  clwwlkvbij  26329  eclclwwlkn1  26359  vdgrun  26428  vdgrfiun  26429  rusgranumwlkb0  26480  rusgra0edg  26482  h2hcau  27220  dfch2  27650  hhcno  28147  hhcnf  28148  pjhmopidm  28426  elpjrn  28433  rabrab  28722  rabid2f  28724  rabfmpunirn  28833  mptctf  28883  maprnin  28894  fpwrelmapffslem  28895  fpwrelmap  28896  sigaex  29499  sigaval  29500  isrnsigaOLD  29502  ballotlem2  29877  bnj1441  30165  bnj110  30182  neibastop3  31527  bj-rababwv  32061  bj-rabbida2  32105  bj-inrab  32115  rabiun  32552  ptrest  32578  poimirlem26  32605  poimirlem27  32606  cnambfre  32628  areacirclem5  32674  ispridlc  33039  lkrval2  33395  lfl1dim  33426  glbconxN  33682  dva1dim  35291  dib1dim2  35475  diclspsn  35501  dih1dimatlem  35636  dihglb2  35649  hdmapoc  36241  eq0rabdioph  36358  rexrabdioph  36376  eldioph4b  36393  aomclem4  36645  clcnvlem  36949  ntrneiel2  37404  rabexgf  38206  ssrabf  38329  rabssf  38334  nb3grprlem1  40608  vtxdun  40696  rusgrprc  40790  ewlksfval  40803  wwlksnfi  41112  wlksnwwlknvbij  41114  rusgrnumwwlkb0  41174  clwwlksvbij  41229  eclclwwlksn1  41259  submgmacs  41594
  Copyright terms: Public domain W3C validator