Definition df-rab 2758

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

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	crab 2753	. 2 class { x e. A | ph }
5	2	cv 1454	. . . . 5 class x
6	5, 3	wcel 1898	. . . 4 wff x e. A
7	6, 1	wa 375	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2448	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1455	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2979  rabid2  2980  rabbi  2981  rabswap  2982  nfrab1  2983  nfrab  2984  rabbiia  3045  rabbidva2  3046  rabeqf  3049  cbvrab  3055  rabab  3077  elrabi  3205  elrabf  3206  elrab3t  3207  ralrab2  3216  rexrab2  3218  cbvrabcsf  3410  dfin5  3424  dfdif2  3425  ss2rab  3517  rabss  3518  ssrab  3519  rabss2  3524  ssrab2  3526  rabssab  3528  notab  3725  unrab  3726  inrab  3727  inrab2  3728  difrab  3729  dfrab3  3730  notrab  3732  rabun2  3734  dfnul3  3746  rabn0  3764  rab0  3765  dfif6  3896  rabeqsn  4013  rabsssn  4014  rabsn  4052  rabsnifsb  4053  reusn  4058  rabsneu  4060  elunirab  4224  elintrab  4260  ssintrab  4272  rabasiun  4296  iunrab  4339  iinrab  4354  intexrab  4576  rmorabex  4674  exss  4677  rabxp  4890  mptpreima  5347  setlikespec  5420  fndmin  6012  fncnvima2  6027  riotauni  6283  riotacl2  6290  snriota  6306  orduniss2  6687  exse2  6759  zfrep6  6788  xp2  6855  unielxp  6856  dfopab2  6874  suppvalbr  6945  ressuppss  6961  rankval3b  8323  scottexs  8384  scott0s  8385  kardex  8391  cardval2  8451  r0weon  8469  axdc2lem  8904  sstskm  9293  negfi  10582  nnzrab  10994  nn0zrab  10995  wrdnval  12733  cshwsexa  12960  shftlem  13180  shftuz  13181  shftdm  13183  hashbc0  15006  cshwsiun  15119  submacs  16661  cycsubg  16894  eqglact  16917  dfrhm2  17994  aspval2  18620  psrbaglefi  18645  znunithash  19184  clsval2  20114  xkoptsub  20718  ptcmplem2  21117  cnblcld  21844  cncmet  22339  shft2rab  22510  sca2rab  22514  vmappw  24092  usgraop  25126  nbgraf1olem5  25222  nb3graprlem1  25228  wwlknprop  25463  wwlknfi  25515  wlknwwlknvbij  25517  clwwlkvbij  25578  eclclwwlkn1  25609  vdgrun  25678  vdgrfiun  25679  rusgranumwlkb0  25730  rusgra0edg  25732  h2hcau  26681  dfch2  27109  hhcno  27606  hhcnf  27607  pjhmopidm  27885  elpjrn  27892  rabrab  28183  rabid2f  28185  rabfmpunirn  28301  mptctf  28354  maprnin  28365  fpwrelmapffslem  28366  fpwrelmap  28367  sigaex  28980  sigaval  28981  isrnsigaOLD  28983  ballotlem2  29370  bnj1441  29701  bnj110  29718  neibastop3  31067  bj-rababwv  31521  bj-rabbida2  31565  bj-inrab  31575  rabiun  31971  ptrest  31984  poimirlem26  32011  poimirlem27  32012  cnambfre  32034  areacirclem5  32081  ispridlc  32348  lkrval2  32701  lfl1dim  32732  glbconxN  32988  dva1dim  34597  dib1dim2  34781  diclspsn  34807  dih1dimatlem  34942  dihglb2  34955  hdmapoc  35547  eq0rabdioph  35664  rexrabdioph  35682  eldioph4b  35699  aomclem4  35960  clcnvlem  36275  rabexgf  37385  prprrab  39114  nb3grprlem1  39504  vtxduhgrun  39588  rusgrprc  39655  ewlksfval  39668  submgmacs  40077