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 3105
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 3100 . 2 class {𝑥𝐴𝜑}
52cv 1636 . . . . 5 class 𝑥
65, 3wcel 2156 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2792 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1637 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3304  rabrab  3305  rabid2  3307  rabid2f  3308  rabbi  3309  rabswap  3310  nfrab1  3311  nfrab  3312  rabbiia  3374  rabbidva2  3376  rabeqf  3380  cbvrab  3388  rabab  3417  elrabi  3554  elrabf  3555  rabeqc  3557  elrab3t  3558  ralrab2  3568  rexrab2  3570  cbvrabcsf  3763  dfin5  3777  dfdif2  3778  ss2rab  3875  rabss  3876  ssrab  3877  rabss2  3882  ssrab2  3884  rabssab  3888  notab  4098  unrab  4099  inrab  4100  inrab2  4101  difrab  4102  dfrab3  4103  notrab  4105  rabun2  4107  dfnul3  4119  rab0  4156  rabeq0  4157  dfif6  4282  rabeqsn  4407  rabsssn  4408  rabsnifsb  4448  reusn  4453  rabsneu  4455  elunirab  4642  elintrab  4681  ssintrab  4692  iunrab  4759  iinrab  4774  intexrab  5015  rmorabex  5118  exss  5121  rabxp  5354  mptpreima  5842  setlikespec  5914  fndmin  6542  fncnvima2  6557  riotauni  6837  riotacl2  6844  snriota  6861  orduniss2  7259  exse2  7331  zfrep6  7360  xp2  7431  unielxp  7432  dfopab2  7450  suppvalbr  7529  ressuppss  7544  rankval3b  8932  scottexs  8993  scott0s  8994  kardex  9000  cardval2  9096  r0weon  9114  axdc2lem  9551  sstskm  9945  negfi  11252  nnzrab  11667  nn0zrab  11668  prprrab  13468  wrdnval  13542  cshwsexa  13790  shftlem  14027  shftuz  14028  shftdm  14030  hashbc0  15922  cshwsiun  16014  submacs  17566  cycsubg  17820  eqglact  17843  dfrhm2  18917  aspval2  19552  psrbaglefi  19577  znunithash  20116  clsval2  21064  xkoptsub  21667  ptcmplem2  22066  cnblcld  22787  cncmet  23327  shft2rab  23485  sca2rab  23489  vmappw  25052  2lgslem1b  25327  nb3grprlem1  26494  vtxdun  26601  rusgrprc  26710  ewlksfval  26721  wwlksnfi  27039  wlksnwwlknvbijOLD  27042  rusgrnumwwlkb0  27109  eclclwwlkn1  27222  clwwlkvbij  27278  clwwlkvbijOLDOLD  27279  clwwlkvbijOLD  27280  h2hcau  28160  dfch2  28590  hhcno  29087  hhcnf  29088  pjhmopidm  29366  elpjrn  29373  rabfmpunirn  29776  mptctf  29818  maprnin  29829  fpwrelmapffslem  29830  fpwrelmap  29831  sigaex  30493  sigaval  30494  isrnsigaOLD  30496  ballotlem2  30871  bnj1441  31229  bnj110  31246  madeval2  32252  neibastop3  32673  bj-rababwv  33170  bj-rabbida2  33218  bj-inrab  33229  rabiun  33690  ptrest  33716  poimirlem26  33743  poimirlem27  33744  cnambfre  33765  areacirclem5  33811  ispridlc  34175  eccnvepres  34357  lkrval2  34865  lfl1dim  34896  glbconxN  35153  dva1dim  36760  dib1dim2  36943  diclspsn  36969  dih1dimatlem  37104  dihglb2  37117  hdmapoc  37706  eq0rabdioph  37836  rexrabdioph  37854  eldioph4b  37871  aomclem4  38122  clcnvlem  38424  ntrneiel2  38878  rabexgf  39671  ssrabf  39784  rabssf  39788  rabbida2  39802  rabbida3  39805  f1oresf1o  41874  f1oresf1o2  41875  sprvalpw  42292  submgmacs  42366
  Copyright terms: Public domain W3C validator