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

Definition df-rab 2516
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 2512 . 2  class  { x  e.  A  |  ph }
52cv 1618 . . . . 5  class  x
65, 3wcel 1621 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2239 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1619 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2675  rabid2  2676  rabbi  2677  rabswap  2678  nfrab1  2679  nfrab  2680  rabbiia  2717  rabeqf  2720  cbvrab  2725  rabab  2743  elrabf  2859  ralrab2  2868  rexrab2  2870  cbvrabcsf  3074  dfin5  3086  dfdif2  3087  ss2rab  3170  rabss  3171  ssrab  3172  rabss2  3177  ssrab2  3179  rabssab  3180  notab  3345  unrab  3346  inrab  3347  inrab2  3348  difrab  3349  dfrab2  3350  dfrab3  3351  notrab  3352  rabun2  3354  dfnul3  3365  rabn0  3381  rab0  3382  dfif6  3473  rabsn  3601  reusn  3604  rabsneu  3606  elunirab  3740  elintrab  3772  ssintrab  3783  iunrab  3847  iinrab  3862  intexrab  4068  exss  4129  orduniss2  4515  rabxp  4632  exse2  4954  mptpreima  5072  fndmin  5484  fncnvima2  5499  zfrep6  5600  xp2  6009  unielxp  6010  dfopab2  6026  riotauni  6197  riotacl2  6204  snriota  6221  supexd  7088  cantnfreslem  7261  rankval3b  7382  scottexs  7441  scott0s  7442  kardex  7448  cardval2  7508  r0weon  7524  dfac2a  7640  axdc2lem  7958  sstskm  8344  nnzrab  9930  nn0zrab  9931  hashbclem  11267  shftlem  11440  shftuz  11441  shftdm  11443  hashbc0  12926  submacs  14277  cycsubg  14480  eqglact  14503  dfrhm2  15333  aspval2  15918  psrbaglefi  15950  znunithash  16350  clsval2  16619  xkoptsub  17180  ptcmplem2  17579  cnblcld  18116  cncmet  18576  shft2rab  18699  sca2rab  18703  vmappw  20186  h2hcau  21389  dfch2  21816  hhcno  22314  hhcnf  22315  pjhmopidm  22593  elpjrn  22600  vdgrun  23064  setlikespec  23355  mapex2  24306  dfdir2  24457  sallnei  24695  intopcoaconb  24706  neibastop3  25477  ispridlc  25861  eq0rabdioph  26022  rexrabdioph  26041  eldioph4b  26060  rencldnfilem  26069  aomclem4  26320  bnj1441  27562  bnj110  27579  lkrval2  27969  lfl1dim  28000  glbconxN  28256  dva1dim  29863  dib1dim2  30047  diclspsn  30073  dih1dimatlem  30208  dihglb2  30221  mapdvalc  30508  mapdval4N  30511  hdmapoc  30813
  Copyright terms: Public domain W3C validator