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

Definition df-rab 2552
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 2547 . 2  class  { x  e.  A  |  ph }
52cv 1622 . . . . 5  class  x
65, 3wcel 1684 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2269 . 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  2716  rabid2  2717  rabbi  2718  rabswap  2719  nfrab1  2720  nfrab  2721  rabbiia  2778  rabeqf  2781  cbvrab  2786  rabab  2805  elrabf  2922  ralrab2  2931  rexrab2  2933  cbvrabcsf  3146  dfin5  3160  dfdif2  3161  ss2rab  3249  rabss  3250  ssrab  3251  rabss2  3256  ssrab2  3258  rabssab  3259  notab  3438  unrab  3439  inrab  3440  inrab2  3441  difrab  3442  dfrab2  3443  dfrab3  3444  notrab  3445  rabun2  3447  dfnul3  3458  rabn0  3474  rab0  3475  dfif6  3568  rabsn  3697  reusn  3700  rabsneu  3702  elunirab  3840  elintrab  3874  ssintrab  3885  iunrab  3949  iinrab  3964  intexrab  4170  rmorabex  4233  exss  4236  orduniss2  4624  rabxp  4725  exse2  5047  mptpreima  5166  fndmin  5632  fncnvima2  5647  zfrep6  5748  xp2  6157  unielxp  6158  dfopab2  6174  riotauni  6311  riotacl2  6318  snriota  6335  cantnfreslem  7377  rankval3b  7498  scottexs  7557  scott0s  7558  kardex  7564  cardval2  7624  r0weon  7640  dfac2a  7756  axdc2lem  8074  sstskm  8464  nnzrab  10051  nn0zrab  10052  hashbclem  11390  shftlem  11563  shftuz  11564  shftdm  11566  hashbc0  13052  submacs  14442  cycsubg  14645  eqglact  14668  dfrhm2  15498  aspval2  16086  psrbaglefi  16118  znunithash  16518  clsval2  16787  xkoptsub  17348  ptcmplem2  17747  cnblcld  18284  cncmet  18744  shft2rab  18867  sca2rab  18871  vmappw  20354  h2hcau  21559  dfch2  21986  hhcno  22484  hhcnf  22485  pjhmopidm  22763  elpjrn  22770  ballotlem2  23047  rabid2f  23135  rabbidva2  23164  rabfmpunirn  23217  mptctf  23348  sigaex  23470  sigaval  23471  isrnsigaOLD  23473  isibfm  23593  vdgrun  23893  setlikespec  24187  areacirclem6  24930  mapex2  25140  dfdir2  25291  sallnei  25529  intopcoaconb  25540  neibastop3  26311  ispridlc  26695  eq0rabdioph  26856  rexrabdioph  26875  eldioph4b  26894  rencldnfilem  26903  aomclem4  27154  rabexgf  27695  isusgra0  28106  bnj1441  28873  bnj110  28890  lkrval2  29280  lfl1dim  29311  glbconxN  29567  dva1dim  31174  dib1dim2  31358  diclspsn  31384  dih1dimatlem  31519  dihglb2  31532  mapdvalc  31819  mapdval4N  31822  hdmapoc  32124
  Copyright terms: Public domain W3C validator