MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rab 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  4804  rabxp  4905  exse2  5229  mptpreima  5354  fndmin  5828  fncnvima2  5843  zfrep6  5959  xp2  6375  unielxp  6376  dfopab2  6392  riotauni  6547  riotacl2  6554  snriota  6571  cantnfreslem  7620  rankval3b  7741  scottexs  7800  scott0s  7801  kardex  7807  cardval2  7867  r0weon  7883  dfac2a  7999  axdc2lem  8317  sstskm  8706  nnzrab  10298  nn0zrab  10299  hashbclem  11689  shftlem  11871  shftuz  11872  shftdm  11874  hashbc0  13361  submacs  14753  cycsubg  14956  eqglact  14979  dfrhm2  15809  aspval2  16393  psrbaglefi  16425  znunithash  16833  clsval2  17102  xkoptsub  17674  ptcmplem2  18072  cnblcld  18797  cncmet  19263  shft2rab  19392  sca2rab  19396  vmappw  20887  isusgra0  21364  nbgraf1olem5  21443  nb3graprlem1  21448  vdgrun  21660  vdgrfiun  21661  h2hcau  22470  dfch2  22897  hhcno  23395  hhcnf  23396  pjhmopidm  23674  elpjrn  23681  rabid2f  23955  rabbidva2  23974  rabfmpunirn  24053  mptctf  24100  sigaex  24480  sigaval  24481  isrnsigaOLD  24483  ballotlem2  24734  setlikespec  25442  rabiun2  26186  cnambfre  26201  areacirclem6  26233  neibastop3  26328  ispridlc  26617  eq0rabdioph  26772  rexrabdioph  26791  eldioph4b  26809  aomclem4  27069  rabexgf  27609  shwrdsiun  28172  bnj1441  29066  bnj110  29083  lkrval2  29727  lfl1dim  29758  glbconxN  30014  dva1dim  31621  dib1dim2  31805  diclspsn  31831  dih1dimatlem  31966  dihglb2  31979  mapdvalc  32266  mapdval4N  32269  hdmapoc  32571
  Copyright terms: Public domain W3C validator