MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rab Unicode version

Definition df-rab 2554
Description: Define a restricted class abstraction (class builder), which is the class of all  x in  A such that  ph is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-rab  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }

Detailed syntax breakdown of Definition df-rab
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  set  x
3 cA . . 3  class  A
41, 2, 3crab 2549 . 2  class  { x  e.  A  |  ph }
52cv 1624 . . . . 5  class  x
65, 3wcel 1686 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2271 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1625 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2718  rabid2  2719  rabbi  2720  rabswap  2721  nfrab1  2722  nfrab  2723  rabbiia  2780  rabeqf  2783  cbvrab  2788  rabab  2807  elrabf  2924  ralrab2  2933  rexrab2  2935  cbvrabcsf  3148  dfin5  3162  dfdif2  3163  ss2rab  3251  rabss  3252  ssrab  3253  rabss2  3258  ssrab2  3260  rabssab  3261  notab  3440  unrab  3441  inrab  3442  inrab2  3443  difrab  3444  dfrab2  3445  dfrab3  3446  notrab  3447  rabun2  3449  dfnul3  3460  rabn0  3476  rab0  3477  dfif6  3570  rabsn  3699  reusn  3702  rabsneu  3704  elunirab  3842  elintrab  3876  ssintrab  3887  iunrab  3951  iinrab  3966  intexrab  4172  rmorabex  4235  exss  4238  orduniss2  4626  rabxp  4727  exse2  5049  mptpreima  5168  fndmin  5634  fncnvima2  5649  zfrep6  5750  xp2  6159  unielxp  6160  dfopab2  6176  riotauni  6313  riotacl2  6320  snriota  6337  cantnfreslem  7379  rankval3b  7500  scottexs  7559  scott0s  7560  kardex  7566  cardval2  7626  r0weon  7642  dfac2a  7758  axdc2lem  8076  sstskm  8466  nnzrab  10053  nn0zrab  10054  hashbclem  11392  shftlem  11565  shftuz  11566  shftdm  11568  hashbc0  13054  submacs  14444  cycsubg  14647  eqglact  14670  dfrhm2  15500  aspval2  16088  psrbaglefi  16120  znunithash  16520  clsval2  16789  xkoptsub  17350  ptcmplem2  17749  cnblcld  18286  cncmet  18746  shft2rab  18869  sca2rab  18873  vmappw  20356  h2hcau  21561  dfch2  21988  hhcno  22486  hhcnf  22487  pjhmopidm  22765  elpjrn  22772  ballotlem2  23049  rabid2f  23137  rabbidva2  23166  rabfmpunirn  23219  mptctf  23350  sigaex  23472  sigaval  23473  isrnsigaOLD  23475  isibfm  23595  vdgrun  23895  setlikespec  24189  rabiun2  24929  areacirclem6  24941  mapex2  25151  dfdir2  25302  sallnei  25540  intopcoaconb  25551  neibastop3  26322  ispridlc  26706  eq0rabdioph  26867  rexrabdioph  26886  eldioph4b  26905  rencldnfilem  26914  aomclem4  27165  rabexgf  27706  isusgra0  28117  bnj1441  28946  bnj110  28963  lkrval2  29353  lfl1dim  29384  glbconxN  29640  dva1dim  31247  dib1dim2  31431  diclspsn  31457  dih1dimatlem  31592  dihglb2  31605  mapdvalc  31892  mapdval4N  31895  hdmapoc  32197
  Copyright terms: Public domain W3C validator