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

Definition df-rab 2527
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 2522 . 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 2244 . 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  2691  rabid2  2692  rabbi  2693  rabswap  2694  nfrab1  2695  nfrab  2696  rabbiia  2753  rabeqf  2756  cbvrab  2761  rabab  2780  elrabf  2897  ralrab2  2906  rexrab2  2908  cbvrabcsf  3121  dfin5  3135  dfdif2  3136  ss2rab  3224  rabss  3225  ssrab  3226  rabss2  3231  ssrab2  3233  rabssab  3234  notab  3413  unrab  3414  inrab  3415  inrab2  3416  difrab  3417  dfrab2  3418  dfrab3  3419  notrab  3420  rabun2  3422  dfnul3  3433  rabn0  3449  rab0  3450  dfif6  3542  rabsn  3671  reusn  3674  rabsneu  3676  elunirab  3814  elintrab  3848  ssintrab  3859  iunrab  3923  iinrab  3938  intexrab  4146  rmorabex  4205  exss  4208  orduniss2  4596  rabxp  4713  exse2  5035  mptpreima  5153  fndmin  5566  fncnvima2  5581  zfrep6  5682  xp2  6091  unielxp  6092  dfopab2  6108  riotauni  6279  riotacl2  6286  snriota  6303  cantnfreslem  7345  rankval3b  7466  scottexs  7525  scott0s  7526  kardex  7532  cardval2  7592  r0weon  7608  dfac2a  7724  axdc2lem  8042  sstskm  8432  nnzrab  10019  nn0zrab  10020  hashbclem  11356  shftlem  11529  shftuz  11530  shftdm  11532  hashbc0  13015  submacs  14405  cycsubg  14608  eqglact  14631  dfrhm2  15461  aspval2  16049  psrbaglefi  16081  znunithash  16481  clsval2  16750  xkoptsub  17311  ptcmplem2  17710  cnblcld  18247  cncmet  18707  shft2rab  18830  sca2rab  18834  vmappw  20317  h2hcau  21520  dfch2  21947  hhcno  22445  hhcnf  22446  pjhmopidm  22724  elpjrn  22731  ballotlem2  23009  vdgrun  23266  setlikespec  23557  mapex2  24508  dfdir2  24659  sallnei  24897  intopcoaconb  24908  neibastop3  25679  ispridlc  26063  eq0rabdioph  26224  rexrabdioph  26243  eldioph4b  26262  rencldnfilem  26271  aomclem4  26522  rabexgf  27064  bnj1441  28005  bnj110  28022  lkrval2  28530  lfl1dim  28561  glbconxN  28817  dva1dim  30424  dib1dim2  30608  diclspsn  30634  dih1dimatlem  30769  dihglb2  30782  mapdvalc  31069  mapdval4N  31072  hdmapoc  31374
  Copyright terms: Public domain W3C validator