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

Definition df-rab 2679
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 2674 . 2  class  { x  e.  A  |  ph }
52cv 1648 . . . . 5  class  x
65, 3wcel 1721 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2394 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1649 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2848  rabid2  2849  rabbi  2850  rabswap  2851  nfrab1  2852  nfrab  2853  rabbiia  2910  rabeqf  2913  cbvrab  2918  rabab  2937  elrabi  3054  elrabf  3055  ralrab2  3064  rexrab2  3066  cbvrabcsf  3278  dfin5  3292  dfdif2  3293  ss2rab  3383  rabss  3384  ssrab  3385  rabss2  3390  ssrab2  3392  rabssab  3394  notab  3575  unrab  3576  inrab  3577  inrab2  3578  difrab  3579  dfrab2  3580  dfrab3  3581  notrab  3582  rabun2  3584  dfnul3  3595  rabn0  3611  rab0  3612  dfif6  3706  rabsn  3837  reusn  3841  rabsneu  3843  elunirab  3992  elintrab  4026  ssintrab  4037  iunrab  4102  iinrab  4117  intexrab  4323  rmorabex  4387  exss  4390  orduniss2  4776  rabxp  4877  exse2  5201  mptpreima  5326  fndmin  5800  fncnvima2  5815  zfrep6  5931  xp2  6347  unielxp  6348  dfopab2  6364  riotauni  6519  riotacl2  6526  snriota  6543  cantnfreslem  7591  rankval3b  7712  scottexs  7771  scott0s  7772  kardex  7778  cardval2  7838  r0weon  7854  dfac2a  7970  axdc2lem  8288  sstskm  8677  nnzrab  10269  nn0zrab  10270  hashbclem  11660  shftlem  11842  shftuz  11843  shftdm  11845  hashbc0  13332  submacs  14724  cycsubg  14927  eqglact  14950  dfrhm2  15780  aspval2  16364  psrbaglefi  16396  znunithash  16804  clsval2  17073  xkoptsub  17643  ptcmplem2  18041  cnblcld  18766  cncmet  19232  shft2rab  19361  sca2rab  19365  vmappw  20856  isusgra0  21333  nbgraf1olem5  21412  nb3graprlem1  21417  vdgrun  21629  vdgrfiun  21630  h2hcau  22439  dfch2  22866  hhcno  23364  hhcnf  23365  pjhmopidm  23643  elpjrn  23650  rabid2f  23924  rabbidva2  23943  rabfmpunirn  24022  mptctf  24069  sigaex  24449  sigaval  24450  isrnsigaOLD  24452  ballotlem2  24703  setlikespec  25405  rabiun2  26143  cnambfre  26158  areacirclem6  26190  neibastop3  26285  ispridlc  26574  eq0rabdioph  26729  rexrabdioph  26748  eldioph4b  26766  aomclem4  27026  rabexgf  27566  bnj1441  28922  bnj110  28939  lkrval2  29577  lfl1dim  29608  glbconxN  29864  dva1dim  31471  dib1dim2  31655  diclspsn  31681  dih1dimatlem  31816  dihglb2  31829  mapdvalc  32116  mapdval4N  32119  hdmapoc  32421
  Copyright terms: Public domain W3C validator