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 2950
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 2945 . 2 class {𝑥𝐴𝜑}
52cv 1522 . . . . 5 class 𝑥
65, 3wcel 2030 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2637 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1523 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3145  rabrab  3146  rabid2  3148  rabid2f  3149  rabbi  3150  rabswap  3151  nfrab1  3152  nfrab  3153  rabbiia  3215  rabbidva2  3217  rabeqf  3221  cbvrab  3229  rabab  3254  elrabi  3391  elrabf  3392  rabeqc  3394  elrab3t  3395  ralrab2  3405  rexrab2  3407  cbvrabcsf  3601  dfin5  3615  dfdif2  3616  ss2rab  3711  rabss  3712  ssrab  3713  rabss2  3718  ssrab2  3720  rabssab  3723  notab  3930  unrab  3931  inrab  3932  inrab2  3933  difrab  3934  dfrab3  3935  notrab  3937  rabun2  3939  dfnul3  3951  rab0  3988  rab0OLD  3989  rabeq0  3990  rabn0OLD  3992  dfif6  4122  rabeqsn  4246  rabsssn  4247  rabsn  4288  rabsnifsb  4289  reusn  4294  rabsneu  4296  elunirab  4480  elintrab  4520  ssintrab  4532  iunrab  4599  iinrab  4614  intexrab  4853  rmorabex  4958  exss  4961  rabxp  5188  mptpreima  5666  setlikespec  5739  fndmin  6364  fncnvima2  6379  riotauni  6657  riotacl2  6664  snriota  6681  orduniss2  7075  exse2  7147  zfrep6  7176  xp2  7247  unielxp  7248  dfopab2  7266  suppvalbr  7344  ressuppss  7359  rankval3b  8727  scottexs  8788  scott0s  8789  kardex  8795  cardval2  8855  r0weon  8873  axdc2lem  9308  sstskm  9702  negfi  11009  nnzrab  11443  nn0zrab  11444  prprrab  13293  wrdnval  13367  cshwsexa  13616  shftlem  13852  shftuz  13853  shftdm  13855  hashbc0  15756  cshwsiun  15853  submacs  17412  cycsubg  17669  eqglact  17692  dfrhm2  18765  aspval2  19395  psrbaglefi  19420  znunithash  19961  clsval2  20902  xkoptsub  21505  ptcmplem2  21904  cnblcld  22625  cncmet  23165  shft2rab  23322  sca2rab  23326  vmappw  24887  2lgslem1b  25162  nb3grprlem1  26326  vtxdun  26433  rusgrprc  26542  ewlksfval  26553  wwlksnfi  26869  wlksnwwlknvbij  26871  rusgrnumwwlkb0  26938  eclclwwlkn1  27039  clwwlkvbij  27088  clwwlkvbijOLD  27089  h2hcau  27964  dfch2  28394  hhcno  28891  hhcnf  28892  pjhmopidm  29170  elpjrn  29177  rabfmpunirn  29581  mptctf  29623  maprnin  29634  fpwrelmapffslem  29635  fpwrelmap  29636  sigaex  30300  sigaval  30301  isrnsigaOLD  30303  ballotlem2  30678  bnj1441  31037  bnj110  31054  madeval2  32061  neibastop3  32482  bj-rababwv  32992  bj-rabbida2  33038  bj-inrab  33048  rabiun  33512  ptrest  33538  poimirlem26  33565  poimirlem27  33566  cnambfre  33588  areacirclem5  33634  ispridlc  33999  eccnvepres  34186  lkrval2  34695  lfl1dim  34726  glbconxN  34982  dva1dim  36590  dib1dim2  36774  diclspsn  36800  dih1dimatlem  36935  dihglb2  36948  hdmapoc  37540  eq0rabdioph  37657  rexrabdioph  37675  eldioph4b  37692  aomclem4  37944  clcnvlem  38247  ntrneiel2  38701  rabexgf  39497  ssrabf  39612  rabssf  39616  rabbida2  39631  rabbida3  39634  sprvalpw  42055  submgmacs  42129
  Copyright terms: Public domain W3C validator