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

Definition df-rab 2658
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 2653 . 2  class  { x  e.  A  |  ph }
52cv 1648 . . . . 5  class  x
65, 3wcel 1717 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2373 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1649 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2827  rabid2  2828  rabbi  2829  rabswap  2830  nfrab1  2831  nfrab  2832  rabbiia  2889  rabeqf  2892  cbvrab  2897  rabab  2916  elrabi  3033  elrabf  3034  ralrab2  3043  rexrab2  3045  cbvrabcsf  3257  dfin5  3271  dfdif2  3272  ss2rab  3362  rabss  3363  ssrab  3364  rabss2  3369  ssrab2  3371  rabssab  3373  notab  3554  unrab  3555  inrab  3556  inrab2  3557  difrab  3558  dfrab2  3559  dfrab3  3560  notrab  3561  rabun2  3563  dfnul3  3574  rabn0  3590  rab0  3591  dfif6  3685  rabsn  3816  reusn  3820  rabsneu  3822  elunirab  3970  elintrab  4004  ssintrab  4015  iunrab  4079  iinrab  4094  intexrab  4300  rmorabex  4364  exss  4367  orduniss2  4753  rabxp  4854  exse2  5178  mptpreima  5303  fndmin  5776  fncnvima2  5791  zfrep6  5907  xp2  6323  unielxp  6324  dfopab2  6340  riotauni  6492  riotacl2  6499  snriota  6516  cantnfreslem  7564  rankval3b  7685  scottexs  7744  scott0s  7745  kardex  7751  cardval2  7811  r0weon  7827  dfac2a  7943  axdc2lem  8261  sstskm  8650  nnzrab  10241  nn0zrab  10242  hashbclem  11628  shftlem  11810  shftuz  11811  shftdm  11813  hashbc0  13300  submacs  14692  cycsubg  14895  eqglact  14918  dfrhm2  15748  aspval2  16332  psrbaglefi  16364  znunithash  16768  clsval2  17037  xkoptsub  17607  ptcmplem2  18005  cnblcld  18680  cncmet  19144  shft2rab  19271  sca2rab  19275  vmappw  20766  isusgra0  21243  nbgraf1olem5  21321  nb3graprlem1  21326  vdgrun  21520  vdgrfiun  21521  h2hcau  22330  dfch2  22757  hhcno  23255  hhcnf  23256  pjhmopidm  23534  elpjrn  23541  rabid2f  23811  rabbidva2  23830  rabfmpunirn  23907  mptctf  23953  sigaex  24288  sigaval  24289  isrnsigaOLD  24291  ballotlem2  24525  setlikespec  25211  rabiun2  25949  areacirclem6  25987  neibastop3  26082  ispridlc  26371  eq0rabdioph  26526  rexrabdioph  26545  eldioph4b  26563  aomclem4  26823  rabexgf  27363  bnj1441  28550  bnj110  28567  lkrval2  29205  lfl1dim  29236  glbconxN  29492  dva1dim  31099  dib1dim2  31283  diclspsn  31309  dih1dimatlem  31444  dihglb2  31457  mapdvalc  31744  mapdval4N  31747  hdmapoc  32049
  Copyright terms: Public domain W3C validator