Definition df-rab 2723

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 2718	. 2 class { x e. A | ph }
5	2	cv 1436	. . . . 5 class x
6	5, 3	wcel 1872	. . . 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  2944  rabid2  2945  rabbi  2946  rabswap  2947  nfrab1  2948  nfrab  2949  rabbiia  3010  rabbidva2  3011  rabeqf  3014  cbvrab  3020  rabab  3041  elrabi  3168  elrabf  3169  elrab3t  3170  ralrab2  3179  rexrab2  3181  cbvrabcsf  3373  dfin5  3387  dfdif2  3388  ss2rab  3480  rabss  3481  ssrab  3482  rabss2  3487  ssrab2  3489  rabssab  3491  notab  3686  unrab  3687  inrab  3688  inrab2  3689  difrab  3690  dfrab3  3691  notrab  3693  rabun2  3695  dfnul3  3707  rabn0  3725  rab0  3726  dfif6  3857  rabsn  4010  rabsnifsb  4011  reusn  4016  rabsneu  4018  elunirab  4174  elintrab  4210  ssintrab  4222  rabasiun  4246  iunrab  4289  iinrab  4304  intexrab  4526  rmorabex  4624  exss  4627  rabxp  4833  mptpreima  5290  setlikespec  5363  fndmin  5948  fncnvima2  5963  riotauni  6217  riotacl2  6224  snriota  6240  orduniss2  6618  exse2  6690  zfrep6  6719  xp2  6786  unielxp  6787  dfopab2  6805  suppvalbr  6873  ressuppss  6889  rankval3b  8249  scottexs  8310  scott0s  8311  kardex  8317  cardval2  8377  r0weon  8395  axdc2lem  8829  sstskm  9218  negfi  10505  nnzrab  10916  nn0zrab  10917  wrdnval  12645  cshwsexa  12869  shftlem  13075  shftuz  13076  shftdm  13078  hashbc0  14900  cshwsiun  15013  submacs  16555  cycsubg  16788  eqglact  16811  dfrhm2  17888  aspval2  18514  psrbaglefi  18539  znunithash  19077  clsval2  20007  xkoptsub  20611  ptcmplem2  21010  cnblcld  21737  cncmet  22232  shft2rab  22403  sca2rab  22407  vmappw  23985  usgraop  25019  nbgraf1olem5  25115  nb3graprlem1  25121  wwlknprop  25356  wwlknfi  25408  wlknwwlknvbij  25410  clwwlkvbij  25471  eclclwwlkn1  25502  vdgrun  25571  vdgrfiun  25572  rusgranumwlkb0  25623  rusgra0edg  25625  h2hcau  26574  dfch2  27002  hhcno  27499  hhcnf  27500  pjhmopidm  27778  elpjrn  27785  rabrab  28077  rabid2f  28079  rabfmpunirn  28198  mptctf  28255  maprnin  28266  fpwrelmapffslem  28267  fpwrelmap  28268  sigaex  28883  sigaval  28884  isrnsigaOLD  28886  ballotlem2  29273  bnj1441  29604  bnj110  29621  neibastop3  30967  bj-rababwv  31387  bj-rabbida2  31431  bj-inrab  31441  rabiun  31833  ptrest  31846  poimirlem26  31873  poimirlem27  31874  cnambfre  31896  areacirclem5  31943  ispridlc  32210  lkrval2  32568  lfl1dim  32599  glbconxN  32855  dva1dim  34464  dib1dim2  34648  diclspsn  34674  dih1dimatlem  34809  dihglb2  34822  hdmapoc  35414  eq0rabdioph  35531  rexrabdioph  35549  eldioph4b  35566  aomclem4  35828  clcnvlem  36143  rabexgf  37261  prprrab  38865  nb3grprlem1  39195  submgmacs  39405  rabeqsn  39714  rabsssn  39715