Definition df-rab 2791

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 2786	. 2 class { x e. A | ph }
5	2	cv 1436	. . . . 5 class x
6	5, 3	wcel 1870	. . . 4 wff x e. A
7	6, 1	wa 370	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2414	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1437	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  3012  rabid2  3013  rabbi  3014  rabswap  3015  nfrab1  3016  nfrab  3017  rabbiia  3076  rabbidva2  3077  rabeqf  3080  cbvrab  3085  rabab  3105  elrabi  3232  elrabf  3233  elrab3t  3234  ralrab2  3243  rexrab2  3245  cbvrabcsf  3436  dfin5  3450  dfdif2  3451  ss2rab  3543  rabss  3544  ssrab  3545  rabss2  3550  ssrab2  3552  rabssab  3554  notab  3749  unrab  3750  inrab  3751  inrab2  3752  difrab  3753  dfrab3  3754  notrab  3756  rabun2  3758  dfnul3  3770  rabn0  3788  rab0  3789  dfif6  3918  rabsn  4070  rabsnifsb  4071  reusn  4076  rabsneu  4078  elunirab  4234  elintrab  4270  ssintrab  4282  rabasiun  4306  iunrab  4349  iinrab  4364  intexrab  4584  rmorabex  4682  exss  4685  rabxp  4891  mptpreima  5348  setlikespec  5420  fndmin  6004  fncnvima2  6019  riotauni  6273  riotacl2  6280  snriota  6296  orduniss2  6674  exse2  6746  zfrep6  6775  xp2  6842  unielxp  6843  dfopab2  6861  suppvalbr  6929  ressuppss  6945  rankval3b  8296  scottexs  8357  scott0s  8358  kardex  8364  cardval2  8424  r0weon  8442  axdc2lem  8876  sstskm  9266  negfi  10554  nnzrab  10965  nn0zrab  10966  wrdnval  12684  cshwsexa  12908  shftlem  13110  shftuz  13111  shftdm  13113  hashbc0  14920  cshwsiun  15033  submacs  16563  cycsubg  16796  eqglact  16819  dfrhm2  17880  aspval2  18506  psrbaglefi  18531  znunithash  19066  clsval2  19996  xkoptsub  20600  ptcmplem2  20999  cnblcld  21706  cncmet  22183  shft2rab  22339  sca2rab  22343  vmappw  23906  usgraop  24923  nbgraf1olem5  25018  nb3graprlem1  25024  wwlknprop  25259  wwlknfi  25311  wlknwwlknvbij  25313  clwwlkvbij  25374  eclclwwlkn1  25405  vdgrun  25474  vdgrfiun  25475  rusgranumwlkb0  25526  rusgra0edg  25528  h2hcau  26467  dfch2  26895  hhcno  27392  hhcnf  27393  pjhmopidm  27671  elpjrn  27678  rabrab  27970  rabid2f  27972  rabfmpunirn  28092  mptctf  28148  maprnin  28159  fpwrelmapffslem  28160  fpwrelmap  28161  sigaex  28770  sigaval  28771  isrnsigaOLD  28773  ballotlem2  29147  bnj1441  29440  bnj110  29457  neibastop3  30803  bj-rababwv  31227  bj-rabbida2  31270  bj-inrab  31280  rabiun  31630  ptrest  31643  poimirlem26  31670  poimirlem27  31671  cnambfre  31693  areacirclem5  31740  ispridlc  32007  lkrval2  32365  lfl1dim  32396  glbconxN  32652  dva1dim  34261  dib1dim2  34445  diclspsn  34471  dih1dimatlem  34606  dihglb2  34619  hdmapoc  35211  eq0rabdioph  35328  rexrabdioph  35346  eldioph4b  35363  aomclem4  35621  rabexgf  36985  submgmacs  38562  rabeqsn  38871  rabsssn  38872