Definition df-rab 2531

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 2526	. 2 class { x e. A | ph }
5	2	cv 1397	. . . . 5 class x
6	5, 3	wcel 2205	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2220	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1398	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2721  rabid2  2723  rabbi  2724  rabswap  2725  nfrab1  2726  nfrabw  2727  rabbidva2  2799  rabbiia  2801  rabeqf  2805  cbvrab  2813  rabab  2837  elrabi  2972  elrabf  2973  elrab3t  2974  ralrab2  2984  rexrab2  2986  cbvrabcsf  3206  dfin5  3220  dfdif2  3221  ss2rab  3316  rabss  3317  ssrab  3318  rabss2  3323  ssrab2  3325  rabssab  3329  notab  3493  unrab  3494  inrab  3495  inrab2  3496  difrab  3497  dfrab2  3498  dfrab3  3499  notrab  3500  rabun2  3502  dfnul3  3513  rabn0r  3537  rabn0m  3538  rab0  3539  rabeq0  3540  dfif6  3624  rabsn  3758  rabsnifsb  3759  reusn  3764  rabsneu  3766  elunirab  3929  elintrab  3963  ssintrab  3974  iunrab  4041  iinrabm  4056  intexrabim  4267  repizf2  4277  exss  4345  rabxp  4789  exse2  5138  mptpreima  5258  fndmin  5787  fncnvima2  5801  riotauni  6012  riotacl2  6020  snriota  6037  xp2  6369  unielxp  6370  dfopab2  6385  ressuppss  6456  unfiexmid  7180  nnzrab  9603  nn0zrab  9604  wrdnval  11259  shftlem  11505  shftuz  11506  shftdm  11511  negfi  11917  eqglact  13959  dfrhm2  14316  cnblcld  15417  2lgslem1b  15979  vtxdfifiun  16309  bdcrab  16639