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

Definition df-rab 2706
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 2701 . 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 2421 . 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  2876  rabid2  2877  rabbi  2878  rabswap  2879  nfrab1  2880  nfrab  2881  rabbiia  2938  rabeqf  2941  cbvrab  2946  rabab  2965  elrabi  3082  elrabf  3083  ralrab2  3092  rexrab2  3094  cbvrabcsf  3306  dfin5  3320  dfdif2  3321  ss2rab  3411  rabss  3412  ssrab  3413  rabss2  3418  ssrab2  3420  rabssab  3422  notab  3603  unrab  3604  inrab  3605  inrab2  3606  difrab  3607  dfrab2  3608  dfrab3  3609  notrab  3610  rabun2  3612  dfnul3  3623  rabn0  3639  rab0  3640  dfif6  3734  rabsn  3865  reusn  3869  rabsneu  3871  elunirab  4020  elintrab  4054  ssintrab  4065  iunrab  4130  iinrab  4145  intexrab  4351  rmorabex  4415  exss  4418  orduniss2  4805  rabxp  4906  exse2  5230  mptpreima  5355  fndmin  5829  fncnvima2  5844  zfrep6  5960  xp2  6376  unielxp  6377  dfopab2  6393  riotauni  6548  riotacl2  6555  snriota  6572  cantnfreslem  7623  rankval3b  7744  scottexs  7803  scott0s  7804  kardex  7810  cardval2  7870  r0weon  7886  dfac2a  8002  axdc2lem  8320  sstskm  8709  nnzrab  10301  nn0zrab  10302  hashbclem  11693  shftlem  11875  shftuz  11876  shftdm  11878  hashbc0  13365  submacs  14757  cycsubg  14960  eqglact  14983  dfrhm2  15813  aspval2  16397  psrbaglefi  16429  znunithash  16837  clsval2  17106  xkoptsub  17678  ptcmplem2  18076  cnblcld  18801  cncmet  19267  shft2rab  19396  sca2rab  19400  vmappw  20891  isusgra0  21368  nbgraf1olem5  21447  nb3graprlem1  21452  vdgrun  21664  vdgrfiun  21665  h2hcau  22474  dfch2  22901  hhcno  23399  hhcnf  23400  pjhmopidm  23678  elpjrn  23685  rabid2f  23959  rabbidva2  23978  rabfmpunirn  24057  mptctf  24104  sigaex  24484  sigaval  24485  isrnsigaOLD  24487  ballotlem2  24738  setlikespec  25454  rabiun2  26230  cnambfre  26245  areacirclem6  26287  neibastop3  26382  ispridlc  26671  eq0rabdioph  26826  rexrabdioph  26845  eldioph4b  26863  aomclem4  27123  rabexgf  27662  cshwsiun  28249  cshwsexa  28254  bnj1441  29149  bnj110  29166  lkrval2  29825  lfl1dim  29856  glbconxN  30112  dva1dim  31719  dib1dim2  31903  diclspsn  31929  dih1dimatlem  32064  dihglb2  32077  mapdvalc  32364  mapdval4N  32367  hdmapoc  32669
  Copyright terms: Public domain W3C validator