Definition df-rab 2818

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 2813	. 2 class { x e. A | ph }
5	2	cv 1373	. . . . 5 class x
6	5, 3	wcel 1762	. . . 4 wff x e. A
7	6, 1	wa 369	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2447	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1374	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  3033  rabid2  3034  rabbi  3035  rabswap  3036  nfrab1  3037  nfrab  3038  rabbiia  3097  rabbidva2  3098  rabeqf  3101  cbvrab  3106  rabab  3126  elrabi  3253  elrabf  3254  elrab3t  3255  ralrab2  3264  rexrab2  3266  cbvrabcsf  3465  dfin5  3479  dfdif2  3480  ss2rab  3571  rabss  3572  ssrab  3573  rabss2  3578  ssrab2  3580  rabssab  3582  notab  3763  unrab  3764  inrab  3765  inrab2  3766  difrab  3767  dfrab3  3768  notrab  3770  rabun2  3772  dfnul3  3783  rabn0  3800  rab0  3801  dfif6  3937  rabsn  4089  rabsnifsb  4090  reusn  4095  rabsneu  4097  elunirab  4252  elintrab  4289  ssintrab  4300  rabasiun  4324  iunrab  4367  iinrab  4382  intexrab  4601  rmorabex  4702  exss  4705  rabxp  5030  mptpreima  5493  fndmin  5981  fncnvima2  5996  riotauni  6244  riotacl2  6252  snriota  6268  orduniss2  6641  exse2  6715  zfrep6  6744  xp2  6811  unielxp  6812  dfopab2  6830  suppvalbr  6897  ressuppss  6911  extmptsuppeq  6916  rankval3b  8235  scottexs  8296  scott0s  8297  kardex  8303  cardval2  8363  r0weon  8381  dfac2a  8501  axdc2lem  8819  sstskm  9211  nnzrab  10883  nn0zrab  10884  hashbclem  12456  wrdnval  12526  cshwsexa  12744  shftlem  12853  shftuz  12854  shftdm  12856  hashbc0  14373  cshwsiun  14433  submacs  15801  cycsubg  16019  eqglact  16042  dfrhm2  17145  aspval2  17762  psrbaglefi  17789  psrbaglefiOLD  17790  znunithash  18365  clsval2  19312  xkoptsub  19885  ptcmplem2  20283  cnblcld  21012  cncmet  21491  shft2rab  21649  sca2rab  21653  vmappw  23113  isusgra0  24012  usgraop  24015  nbgraf1olem5  24109  nb3graprlem1  24115  wwlknprop  24350  wwlkextwrd  24392  wwlknfi  24402  wlknwwlknvbij  24404  clwwlkvbij  24465  eclclwwlkn1  24496  vdgrun  24565  vdgrfiun  24566  rusgranumwlkl1  24611  rusgranumwlklem3  24615  rusgranumwlkb0  24617  rusgra0edg  24619  numclwwlkovf2  24749  h2hcau  25560  dfch2  25989  hhcno  26487  hhcnf  26488  pjhmopidm  26766  elpjrn  26773  rabrab  27063  rabid2f  27064  rabfmpunirn  27151  mptctf  27204  maprnin  27214  fpwrelmapffslem  27215  fpwrelmap  27216  sigaex  27737  sigaval  27738  isrnsigaOLD  27740  ballotlem2  28055  setlikespec  28832  rabiun  29601  ptrest  29614  cnambfre  29629  areacirclem5  29677  neibastop3  29772  ispridlc  30059  eq0rabdioph  30303  rexrabdioph  30320  eldioph4b  30338  aomclem4  30598  rabexgf  30934  rabeqsn  31860  rabsssn  31861  bnj1441  32855  bnj110  32872  bj-rababwv  33401  bj-rabbida2  33443  bj-inrab  33453  lkrval2  33764  lfl1dim  33795  glbconxN  34051  dva1dim  35658  dib1dim2  35842  diclspsn  35868  dih1dimatlem  36003  dihglb2  36016  mapdvalc  36303  mapdval4N  36306  hdmapoc  36608