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 3051
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 3046 . 2 class {𝑥𝐴𝜑}
52cv 1623 . . . . 5 class 𝑥
65, 3wcel 2131 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2738 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1624 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3246  rabrab  3247  rabid2  3249  rabid2f  3250  rabbi  3251  rabswap  3252  nfrab1  3253  nfrab  3254  rabbiia  3316  rabbidva2  3318  rabeqf  3322  cbvrab  3330  rabab  3355  elrabi  3491  elrabf  3492  rabeqc  3494  elrab3t  3495  ralrab2  3505  rexrab2  3507  cbvrabcsf  3701  dfin5  3715  dfdif2  3716  ss2rab  3811  rabss  3812  ssrab  3813  rabss2  3818  ssrab2  3820  rabssab  3824  notab  4032  unrab  4033  inrab  4034  inrab2  4035  difrab  4036  dfrab3  4037  notrab  4039  rabun2  4041  dfnul3  4053  rab0  4090  rab0OLD  4091  rabeq0  4092  rabn0OLD  4094  dfif6  4225  rabeqsn  4350  rabsssn  4351  rabsn  4392  rabsnifsb  4393  reusn  4398  rabsneu  4400  elunirab  4592  elintrab  4632  ssintrab  4644  iunrab  4711  iinrab  4726  intexrab  4964  rmorabex  5069  exss  5072  rabxp  5303  mptpreima  5781  setlikespec  5854  fndmin  6479  fncnvima2  6494  riotauni  6772  riotacl2  6779  snriota  6796  orduniss2  7190  exse2  7262  zfrep6  7291  xp2  7362  unielxp  7363  dfopab2  7381  suppvalbr  7459  ressuppss  7474  rankval3b  8854  scottexs  8915  scott0s  8916  kardex  8922  cardval2  8999  r0weon  9017  axdc2lem  9454  sstskm  9848  negfi  11155  nnzrab  11589  nn0zrab  11590  prprrab  13439  wrdnval  13513  cshwsexa  13762  shftlem  13999  shftuz  14000  shftdm  14002  hashbc0  15903  cshwsiun  16000  submacs  17558  cycsubg  17815  eqglact  17838  dfrhm2  18911  aspval2  19541  psrbaglefi  19566  znunithash  20107  clsval2  21048  xkoptsub  21651  ptcmplem2  22050  cnblcld  22771  cncmet  23311  shft2rab  23468  sca2rab  23472  vmappw  25033  2lgslem1b  25308  nb3grprlem1  26472  vtxdun  26579  rusgrprc  26688  ewlksfval  26699  wwlksnfi  27016  wlksnwwlknvbij  27018  rusgrnumwwlkb0  27085  eclclwwlkn1  27198  clwwlkvbij  27254  clwwlkvbijOLD  27255  h2hcau  28137  dfch2  28567  hhcno  29064  hhcnf  29065  pjhmopidm  29343  elpjrn  29350  rabfmpunirn  29754  mptctf  29796  maprnin  29807  fpwrelmapffslem  29808  fpwrelmap  29809  sigaex  30473  sigaval  30474  isrnsigaOLD  30476  ballotlem2  30851  bnj1441  31210  bnj110  31227  madeval2  32234  neibastop3  32655  bj-rababwv  33165  bj-rabbida2  33211  bj-inrab  33221  rabiun  33687  ptrest  33713  poimirlem26  33740  poimirlem27  33741  cnambfre  33763  areacirclem5  33809  ispridlc  34174  eccnvepres  34361  lkrval2  34872  lfl1dim  34903  glbconxN  35159  dva1dim  36767  dib1dim2  36951  diclspsn  36977  dih1dimatlem  37112  dihglb2  37125  hdmapoc  37717  eq0rabdioph  37834  rexrabdioph  37852  eldioph4b  37869  aomclem4  38121  clcnvlem  38424  ntrneiel2  38878  rabexgf  39674  ssrabf  39789  rabssf  39793  rabbida2  39808  rabbida3  39811  sprvalpw  42232  submgmacs  42306
  Copyright terms: Public domain W3C validator