Definition df-rab 2921

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 2916	. 2 class { x e. A | ph }
5	2	cv 1482	. . . . 5 class x
6	5, 3	wcel 1990	. . . 4 wff x e. A
7	6, 1	wa 384	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2608	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1483	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  3116  rabid2  3118  rabid2f  3119  rabbi  3120  rabswap  3121  nfrab1  3122  nfrab  3123  rabbiia  3185  rabbidva2  3186  rabeqf  3190  cbvrab  3198  rabab  3223  elrabi  3359  elrabf  3360  elrab3t  3362  ralrab2  3372  rexrab2  3374  cbvrabcsf  3568  dfin5  3582  dfdif2  3583  ss2rab  3678  rabss  3679  ssrab  3680  rabss2  3685  ssrab2  3687  rabssab  3690  notab  3897  unrab  3898  inrab  3899  inrab2  3900  difrab  3901  dfrab3  3902  notrab  3904  rabun2  3906  dfnul3  3918  rab0  3955  rab0OLD  3956  rabeq0  3957  rabn0OLD  3959  dfif6  4089  rabeqsn  4214  rabsssn  4215  rabsn  4256  rabsnifsb  4257  reusn  4262  rabsneu  4264  elunirab  4448  elintrab  4488  ssintrab  4500  iunrab  4567  iinrab  4582  intexrab  4823  rmorabex  4928  exss  4931  rabxp  5154  mptpreima  5628  setlikespec  5701  fndmin  6324  fncnvima2  6339  riotauni  6617  riotacl2  6624  snriota  6641  orduniss2  7033  exse2  7105  zfrep6  7134  xp2  7203  unielxp  7204  dfopab2  7222  suppvalbr  7299  ressuppss  7314  rankval3b  8689  scottexs  8750  scott0s  8751  kardex  8757  cardval2  8817  r0weon  8835  axdc2lem  9270  sstskm  9664  negfi  10971  nnzrab  11405  nn0zrab  11406  prprrab  13255  wrdnval  13335  cshwsexa  13570  shftlem  13808  shftuz  13809  shftdm  13811  hashbc0  15709  cshwsiun  15806  submacs  17365  cycsubg  17622  eqglact  17645  dfrhm2  18717  aspval2  19347  psrbaglefi  19372  znunithash  19913  clsval2  20854  xkoptsub  21457  ptcmplem2  21857  cnblcld  22578  cncmet  23119  shft2rab  23276  sca2rab  23280  vmappw  24842  2lgslem1b  25117  nb3grprlem1  26282  vtxdun  26377  rusgrprc  26486  ewlksfval  26497  wwlksnfi  26801  wlksnwwlknvbij  26803  rusgrnumwwlkb0  26866  clwwlksvbij  26922  eclclwwlksn1  26952  h2hcau  27836  dfch2  28266  hhcno  28763  hhcnf  28764  pjhmopidm  29042  elpjrn  29049  rabrab  29338  rabfmpunirn  29453  mptctf  29495  maprnin  29506  fpwrelmapffslem  29507  fpwrelmap  29508  sigaex  30172  sigaval  30173  isrnsigaOLD  30175  ballotlem2  30550  bnj1441  30911  bnj110  30928  madeval2  31936  neibastop3  32357  bj-rababwv  32867  bj-rabbida2  32913  bj-inrab  32923  rabiun  33382  ptrest  33408  poimirlem26  33435  poimirlem27  33436  cnambfre  33458  areacirclem5  33504  ispridlc  33869  eccnvepres  34045  lkrval2  34377  lfl1dim  34408  glbconxN  34664  dva1dim  36273  dib1dim2  36457  diclspsn  36483  dih1dimatlem  36618  dihglb2  36631  hdmapoc  37223  eq0rabdioph  37340  rexrabdioph  37358  eldioph4b  37375  aomclem4  37627  clcnvlem  37930  ntrneiel2  38384  rabexgf  39183  ssrabf  39298  rabssf  39302  rabbida2  39317  rabbida3  39320  sprvalpw  41730  submgmacs  41804