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

Definition df-rab 2565
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 2560 . 2  class  { x  e.  A  |  ph }
52cv 1631 . . . . 5  class  x
65, 3wcel 1696 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2282 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1632 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2729  rabid2  2730  rabbi  2731  rabswap  2732  nfrab1  2733  nfrab  2734  rabbiia  2791  rabeqf  2794  cbvrab  2799  rabab  2818  elrabf  2935  ralrab2  2944  rexrab2  2946  cbvrabcsf  3159  dfin5  3173  dfdif2  3174  ss2rab  3262  rabss  3263  ssrab  3264  rabss2  3269  ssrab2  3271  rabssab  3272  notab  3451  unrab  3452  inrab  3453  inrab2  3454  difrab  3455  dfrab2  3456  dfrab3  3457  notrab  3458  rabun2  3460  dfnul3  3471  rabn0  3487  rab0  3488  dfif6  3581  rabsn  3710  reusn  3713  rabsneu  3715  elunirab  3856  elintrab  3890  ssintrab  3901  iunrab  3965  iinrab  3980  intexrab  4186  rmorabex  4249  exss  4252  orduniss2  4640  rabxp  4741  exse2  5063  mptpreima  5182  fndmin  5648  fncnvima2  5663  zfrep6  5764  xp2  6173  unielxp  6174  dfopab2  6190  riotauni  6327  riotacl2  6334  snriota  6351  cantnfreslem  7393  rankval3b  7514  scottexs  7573  scott0s  7574  kardex  7580  cardval2  7640  r0weon  7656  dfac2a  7772  axdc2lem  8090  sstskm  8480  nnzrab  10067  nn0zrab  10068  hashbclem  11406  shftlem  11579  shftuz  11580  shftdm  11582  hashbc0  13068  submacs  14458  cycsubg  14661  eqglact  14684  dfrhm2  15514  aspval2  16102  psrbaglefi  16134  znunithash  16534  clsval2  16803  xkoptsub  17364  ptcmplem2  17763  cnblcld  18300  cncmet  18760  shft2rab  18883  sca2rab  18887  vmappw  20370  h2hcau  21575  dfch2  22002  hhcno  22500  hhcnf  22501  pjhmopidm  22779  elpjrn  22786  ballotlem2  23063  rabid2f  23151  rabbidva2  23180  rabfmpunirn  23232  mptctf  23363  sigaex  23485  sigaval  23486  isrnsigaOLD  23488  isibfm  23608  vdgrun  23908  setlikespec  24258  rabiun2  24997  areacirclem6  25033  mapex2  25243  dfdir2  25394  sallnei  25632  intopcoaconb  25643  neibastop3  26414  ispridlc  26798  eq0rabdioph  26959  rexrabdioph  26978  eldioph4b  26997  rencldnfilem  27006  aomclem4  27257  rabexgf  27798  isusgra0  28238  nb3graprlem1  28287  bnj1441  29189  bnj110  29206  lkrval2  29902  lfl1dim  29933  glbconxN  30189  dva1dim  31796  dib1dim2  31980  diclspsn  32006  dih1dimatlem  32141  dihglb2  32154  mapdvalc  32441  mapdval4N  32444  hdmapoc  32746
  Copyright terms: Public domain W3C validator