Definition df-rab 2741

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 2736	. 2 class { x e. A | ph }
5	2	cv 1398	. . . . 5 class x
6	5, 3	wcel 1826	. . . 4 wff x e. A
7	6, 1	wa 367	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2367	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1399	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2959  rabid2  2960  rabbi  2961  rabswap  2962  nfrab1  2963  nfrab  2964  rabbiia  3023  rabbidva2  3024  rabeqf  3027  cbvrab  3032  rabab  3052  elrabi  3179  elrabf  3180  elrab3t  3181  ralrab2  3190  rexrab2  3192  cbvrabcsf  3383  dfin5  3397  dfdif2  3398  ss2rab  3490  rabss  3491  ssrab  3492  rabss2  3497  ssrab2  3499  rabssab  3501  notab  3693  unrab  3694  inrab  3695  inrab2  3696  difrab  3697  dfrab3  3698  notrab  3700  rabun2  3702  dfnul3  3714  rabn0  3732  rab0  3733  dfif6  3860  rabsn  4011  rabsnifsb  4012  reusn  4017  rabsneu  4019  elunirab  4175  elintrab  4211  ssintrab  4223  rabasiun  4247  iunrab  4290  iinrab  4305  intexrab  4524  rmorabex  4622  exss  4625  rabxp  4950  mptpreima  5408  fndmin  5896  fncnvima2  5911  riotauni  6164  riotacl2  6171  snriota  6187  orduniss2  6567  exse2  6638  zfrep6  6667  xp2  6734  unielxp  6735  dfopab2  6753  suppvalbr  6821  ressuppss  6837  rankval3b  8157  scottexs  8218  scott0s  8219  kardex  8225  cardval2  8285  r0weon  8303  axdc2lem  8741  sstskm  9131  nnzrab  10809  nn0zrab  10810  wrdnval  12479  cshwsexa  12703  shftlem  12903  shftuz  12904  shftdm  12906  hashbc0  14525  cshwsiun  14586  submacs  16113  cycsubg  16346  eqglact  16369  dfrhm2  17479  aspval2  18109  psrbaglefi  18136  psrbaglefiOLD  18137  znunithash  18694  clsval2  19636  xkoptsub  20240  ptcmplem2  20638  cnblcld  21367  cncmet  21846  shft2rab  22004  sca2rab  22008  vmappw  23507  usgraop  24471  nbgraf1olem5  24566  nb3graprlem1  24572  wwlknprop  24807  wwlknfi  24859  wlknwwlknvbij  24861  clwwlkvbij  24922  eclclwwlkn1  24953  vdgrun  25022  vdgrfiun  25023  rusgranumwlkb0  25074  rusgra0edg  25076  h2hcau  26013  dfch2  26442  hhcno  26939  hhcnf  26940  pjhmopidm  27218  elpjrn  27225  rabrab  27516  rabid2f  27518  rabfmpunirn  27631  mptctf  27693  maprnin  27704  fpwrelmapffslem  27705  fpwrelmap  27706  sigaex  28258  sigaval  28259  isrnsigaOLD  28261  ballotlem2  28610  setlikespec  29432  rabiun  30201  ptrest  30213  cnambfre  30228  areacirclem5  30277  neibastop3  30346  ispridlc  30633  eq0rabdioph  30875  rexrabdioph  30893  eldioph4b  30910  aomclem4  31169  rabexgf  31566  submgmacs  32810  rabeqsn  33119  rabsssn  33120  bnj1441  34246  bnj110  34263  bj-rababwv  34790  bj-rabbida2  34832  bj-inrab  34842  lkrval2  35228  lfl1dim  35259  glbconxN  35515  dva1dim  37124  dib1dim2  37308  diclspsn  37334  dih1dimatlem  37469  dihglb2  37482  hdmapoc  38074