Definition df-rab 2494

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 2489	. 2 class { x e. A | ph }
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2177	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2192	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1373	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2683  rabid2  2684  rabbi  2685  rabswap  2686  nfrab1  2687  nfrabw  2688  rabbiia  2758  rabbidva2  2760  rabeqf  2763  cbvrab  2771  rabab  2795  elrabi  2930  elrabf  2931  elrab3t  2932  ralrab2  2942  rexrab2  2944  cbvrabcsf  3163  dfin5  3177  dfdif2  3178  ss2rab  3273  rabss  3274  ssrab  3275  rabss2  3280  ssrab2  3282  rabssab  3285  notab  3447  unrab  3448  inrab  3449  inrab2  3450  difrab  3451  dfrab2  3452  dfrab3  3453  notrab  3454  rabun2  3456  dfnul3  3467  rabn0r  3491  rabn0m  3492  rab0  3493  rabeq0  3494  dfif6  3577  rabsn  3705  reusn  3709  rabsneu  3711  elunirab  3869  elintrab  3903  ssintrab  3914  iunrab  3981  iinrabm  3996  intexrabim  4205  repizf2  4214  exss  4279  rabxp  4720  exse2  5065  mptpreima  5185  fndmin  5700  fncnvima2  5714  riotauni  5919  riotacl2  5926  snriota  5942  xp2  6272  unielxp  6273  dfopab2  6288  unfiexmid  7030  nnzrab  9416  nn0zrab  9417  wrdnval  11046  shftlem  11202  shftuz  11203  shftdm  11208  negfi  11614  eqglact  13636  dfrhm2  13991  cnblcld  15082  2lgslem1b  15641  if0ab  15880  bdcrab  15926