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

Definition df-rab 2714
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 2709 . 2  class  { x  e.  A  |  ph }
52cv 1651 . . . . 5  class  x
65, 3wcel 1725 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2422 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1652 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2884  rabid2  2885  rabbi  2886  rabswap  2887  nfrab1  2888  nfrab  2889  rabbiia  2946  rabeqf  2949  cbvrab  2954  rabab  2973  elrabi  3090  elrabf  3091  ralrab2  3100  rexrab2  3102  cbvrabcsf  3314  dfin5  3328  dfdif2  3329  ss2rab  3419  rabss  3420  ssrab  3421  rabss2  3426  ssrab2  3428  rabssab  3430  notab  3611  unrab  3612  inrab  3613  inrab2  3614  difrab  3615  dfrab2  3616  dfrab3  3617  notrab  3618  rabun2  3620  dfnul3  3631  rabn0  3647  rab0  3648  dfif6  3742  rabsn  3873  reusn  3877  rabsneu  3879  elunirab  4028  elintrab  4062  ssintrab  4073  iunrab  4138  iinrab  4153  intexrab  4359  rmorabex  4423  exss  4426  orduniss2  4813  rabxp  4914  exse2  5238  mptpreima  5363  fndmin  5837  fncnvima2  5852  zfrep6  5968  xp2  6384  unielxp  6385  dfopab2  6401  riotauni  6556  riotacl2  6563  snriota  6580  cantnfreslem  7631  rankval3b  7752  scottexs  7811  scott0s  7812  kardex  7818  cardval2  7878  r0weon  7894  dfac2a  8010  axdc2lem  8328  sstskm  8717  nnzrab  10309  nn0zrab  10310  hashbclem  11701  shftlem  11883  shftuz  11884  shftdm  11886  hashbc0  13373  submacs  14765  cycsubg  14968  eqglact  14991  dfrhm2  15821  aspval2  16405  psrbaglefi  16437  znunithash  16845  clsval2  17114  xkoptsub  17686  ptcmplem2  18084  cnblcld  18809  cncmet  19275  shft2rab  19404  sca2rab  19408  vmappw  20899  isusgra0  21376  nbgraf1olem5  21455  nb3graprlem1  21460  vdgrun  21672  vdgrfiun  21673  h2hcau  22482  dfch2  22909  hhcno  23407  hhcnf  23408  pjhmopidm  23686  elpjrn  23693  rabid2f  23967  rabbidva2  23986  rabfmpunirn  24065  mptctf  24112  sigaex  24492  sigaval  24493  isrnsigaOLD  24495  ballotlem2  24746  setlikespec  25462  rabiun  26236  cnambfre  26255  areacirclem5  26296  neibastop3  26391  ispridlc  26680  eq0rabdioph  26835  rexrabdioph  26854  eldioph4b  26872  aomclem4  27132  rabexgf  27671  cshwsiun  28286  cshwsexa  28291  bnj1441  29212  bnj110  29229  lkrval2  29888  lfl1dim  29919  glbconxN  30175  dva1dim  31782  dib1dim2  31966  diclspsn  31992  dih1dimatlem  32127  dihglb2  32140  mapdvalc  32427  mapdval4N  32430  hdmapoc  32732
  Copyright terms: Public domain W3C validator