Definition df-rab 2332

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 2327	. 2 class { x e. A | ph }
5	2	cv 1258	. . . . 5 class x
6	5, 3	wcel 1409	. . . 4 wff x e. A
7	6, 1	wa 101	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2042	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1259	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2502  rabid2  2503  rabbi  2504  rabswap  2505  nfrab1  2506  nfrabxy  2507  rabbiia  2564  rabeqf  2567  cbvrab  2572  rabab  2592  elrabi  2717  elrabf  2718  elrab3t  2719  ralrab2  2728  rexrab2  2730  cbvrabcsf  2938  dfin5  2952  dfdif2  2953  ss2rab  3043  rabss  3044  ssrab  3045  rabss2  3050  ssrab2  3052  rabssab  3054  notab  3234  unrab  3235  inrab  3236  inrab2  3237  difrab  3238  dfrab2  3239  dfrab3  3240  notrab  3241  rabun2  3243  dfnul3  3254  rabn0r  3271  rabn0m  3272  rab0  3273  rabeq0  3274  dfif6  3360  rabsn  3464  reusn  3468  rabsneu  3470  elunirab  3620  elintrab  3654  ssintrab  3665  iunrab  3731  iinrabm  3746  intexrabim  3934  repizf2  3942  exss  3990  rabxp  4407  exse2  4726  mptpreima  4841  fndmin  5301  fncnvima2  5315  riotauni  5501  riotacl2  5508  snriota  5524  xp2  5826  unielxp  5827  dfopab2  5842  nnzrab  8325  nn0zrab  8326  shftlem  9644  shftuz  9645  shftdm  9650  bdcrab  10338