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

Definition df-rab 2553
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 2548 . 2  class  { x  e.  A  |  ph }
52cv 1622 . . . . 5  class  x
65, 3wcel 1685 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2270 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1623 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2717  rabid2  2718  rabbi  2719  rabswap  2720  nfrab1  2721  nfrab  2722  rabbiia  2779  rabeqf  2782  cbvrab  2787  rabab  2806  elrabf  2923  ralrab2  2932  rexrab2  2934  cbvrabcsf  3147  dfin5  3161  dfdif2  3162  ss2rab  3250  rabss  3251  ssrab  3252  rabss2  3257  ssrab2  3259  rabssab  3260  notab  3439  unrab  3440  inrab  3441  inrab2  3442  difrab  3443  dfrab2  3444  dfrab3  3445  notrab  3446  rabun2  3448  dfnul3  3459  rabn0  3475  rab0  3476  dfif6  3569  rabsn  3698  reusn  3701  rabsneu  3703  elunirab  3841  elintrab  3875  ssintrab  3886  iunrab  3950  iinrab  3965  intexrab  4173  rmorabex  4232  exss  4235  orduniss2  4623  rabxp  4724  exse2  5046  mptpreima  5164  fndmin  5594  fncnvima2  5609  zfrep6  5710  xp2  6119  unielxp  6120  dfopab2  6136  riotauni  6307  riotacl2  6314  snriota  6331  cantnfreslem  7373  rankval3b  7494  scottexs  7553  scott0s  7554  kardex  7560  cardval2  7620  r0weon  7636  dfac2a  7752  axdc2lem  8070  sstskm  8460  nnzrab  10047  nn0zrab  10048  hashbclem  11386  shftlem  11559  shftuz  11560  shftdm  11562  hashbc0  13048  submacs  14438  cycsubg  14641  eqglact  14664  dfrhm2  15494  aspval2  16082  psrbaglefi  16114  znunithash  16514  clsval2  16783  xkoptsub  17344  ptcmplem2  17743  cnblcld  18280  cncmet  18740  shft2rab  18863  sca2rab  18867  vmappw  20350  h2hcau  21555  dfch2  21982  hhcno  22480  hhcnf  22481  pjhmopidm  22759  elpjrn  22766  ballotlem2  23043  vdgrun  23300  setlikespec  23591  areacirclem6  24340  mapex2  24551  dfdir2  24702  sallnei  24940  intopcoaconb  24951  neibastop3  25722  ispridlc  26106  eq0rabdioph  26267  rexrabdioph  26286  eldioph4b  26305  rencldnfilem  26314  aomclem4  26565  rabexgf  27106  bnj1441  28152  bnj110  28169  lkrval2  28559  lfl1dim  28590  glbconxN  28846  dva1dim  30453  dib1dim2  30637  diclspsn  30663  dih1dimatlem  30798  dihglb2  30811  mapdvalc  31098  mapdval4N  31101  hdmapoc  31403
  Copyright terms: Public domain W3C validator