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

Definition df-rab 2523
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 2519 . 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 2242 . 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  2684  rabid2  2685  rabbi  2686  rabswap  2687  nfrab1  2688  nfrab  2689  rabbiia  2730  rabeqf  2733  cbvrab  2738  rabab  2756  elrabf  2873  ralrab2  2882  rexrab2  2884  cbvrabcsf  3088  dfin5  3102  dfdif2  3103  ss2rab  3191  rabss  3192  ssrab  3193  rabss2  3198  ssrab2  3200  rabssab  3201  notab  3380  unrab  3381  inrab  3382  inrab2  3383  difrab  3384  dfrab2  3385  dfrab3  3386  notrab  3387  rabun2  3389  dfnul3  3400  rabn0  3416  rab0  3417  dfif6  3509  rabsn  3638  reusn  3641  rabsneu  3643  elunirab  3781  elintrab  3815  ssintrab  3826  iunrab  3890  iinrab  3905  intexrab  4112  exss  4173  orduniss2  4561  rabxp  4678  exse2  5000  mptpreima  5118  fndmin  5531  fncnvima2  5546  zfrep6  5647  xp2  6056  unielxp  6057  dfopab2  6073  riotauni  6244  riotacl2  6251  snriota  6268  supexd  7137  cantnfreslem  7310  rankval3b  7431  scottexs  7490  scott0s  7491  kardex  7497  cardval2  7557  r0weon  7573  dfac2a  7689  axdc2lem  8007  sstskm  8397  nnzrab  9983  nn0zrab  9984  hashbclem  11320  shftlem  11493  shftuz  11494  shftdm  11496  hashbc0  12979  submacs  14369  cycsubg  14572  eqglact  14595  dfrhm2  15425  aspval2  16013  psrbaglefi  16045  znunithash  16445  clsval2  16714  xkoptsub  17275  ptcmplem2  17674  cnblcld  18211  cncmet  18671  shft2rab  18794  sca2rab  18798  vmappw  20281  h2hcau  21484  dfch2  21911  hhcno  22409  hhcnf  22410  pjhmopidm  22688  elpjrn  22695  ballotlem2  22973  vdgrun  23230  setlikespec  23521  mapex2  24472  dfdir2  24623  sallnei  24861  intopcoaconb  24872  neibastop3  25643  ispridlc  26027  eq0rabdioph  26188  rexrabdioph  26207  eldioph4b  26226  rencldnfilem  26235  aomclem4  26486  rabexgf  27028  bnj1441  27885  bnj110  27902  lkrval2  28410  lfl1dim  28441  glbconxN  28697  dva1dim  30304  dib1dim2  30488  diclspsn  30514  dih1dimatlem  30649  dihglb2  30662  mapdvalc  30949  mapdval4N  30952  hdmapoc  31254
  Copyright terms: Public domain W3C validator