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

Definition df-rab 2720
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 2715 . 2  class  { x  e.  A  |  ph }
52cv 1652 . . . . 5  class  x
65, 3wcel 1727 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2428 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1653 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2890  rabid2  2891  rabbi  2892  rabswap  2893  nfrab1  2894  nfrab  2895  rabbiia  2952  rabeqf  2955  cbvrab  2960  rabab  2979  elrabi  3096  elrabf  3097  ralrab2  3106  rexrab2  3108  cbvrabcsf  3300  dfin5  3314  dfdif2  3315  ss2rab  3405  rabss  3406  ssrab  3407  rabss2  3412  ssrab2  3414  rabssab  3416  notab  3596  unrab  3597  inrab  3598  inrab2  3599  difrab  3600  dfrab2  3601  dfrab3  3602  notrab  3603  rabun2  3605  dfnul3  3616  rabn0  3632  rab0  3633  dfif6  3766  rabsn  3897  reusn  3901  rabsneu  3903  elunirab  4052  elintrab  4086  ssintrab  4097  iunrab  4162  iinrab  4177  intexrab  4388  rmorabex  4452  exss  4455  orduniss2  4842  rabxp  4943  exse2  5267  mptpreima  5392  fndmin  5866  fncnvima2  5881  zfrep6  5997  xp2  6413  unielxp  6414  dfopab2  6430  riotauni  6585  riotacl2  6592  snriota  6609  cantnfreslem  7660  rankval3b  7781  scottexs  7842  scott0s  7843  kardex  7849  cardval2  7909  r0weon  7925  dfac2a  8041  axdc2lem  8359  sstskm  8748  nnzrab  10340  nn0zrab  10341  hashbclem  11732  shftlem  11914  shftuz  11915  shftdm  11917  hashbc0  13404  submacs  14796  cycsubg  14999  eqglact  15022  dfrhm2  15852  aspval2  16436  psrbaglefi  16468  znunithash  16876  clsval2  17145  xkoptsub  17717  ptcmplem2  18115  cnblcld  18840  cncmet  19306  shft2rab  19435  sca2rab  19439  vmappw  20930  isusgra0  21407  nbgraf1olem5  21486  nb3graprlem1  21491  vdgrun  21703  vdgrfiun  21704  h2hcau  22513  dfch2  22940  hhcno  23438  hhcnf  23439  pjhmopidm  23717  elpjrn  23724  rabid2f  23998  rabbidva2  24017  rabfmpunirn  24096  mptctf  24143  sigaex  24523  sigaval  24524  isrnsigaOLD  24526  ballotlem2  24777  setlikespec  25493  rabiun  26267  cnambfre  26291  areacirclem5  26334  neibastop3  26429  ispridlc  26718  eq0rabdioph  26873  rexrabdioph  26892  eldioph4b  26910  aomclem4  27170  rabexgf  27709  cshwsiun  28344  cshwsexa  28349  wwlknprop  28392  bnj1441  29310  bnj110  29327  lkrval2  29986  lfl1dim  30017  glbconxN  30273  dva1dim  31880  dib1dim2  32064  diclspsn  32090  dih1dimatlem  32225  dihglb2  32238  mapdvalc  32525  mapdval4N  32528  hdmapoc  32830
  Copyright terms: Public domain W3C validator