Definition df-rab 2384

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 2379	. 2 class { x e. A | ph }
5	2	cv 1298	. . . . 5 class x
6	5, 3	wcel 1448	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2086	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1299	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2564  rabid2  2565  rabbi  2566  rabswap  2567  nfrab1  2568  nfrabxy  2569  rabbiia  2626  rabbidva2  2628  rabeqf  2631  cbvrab  2639  rabab  2662  elrabi  2790  elrabf  2791  elrab3t  2792  ralrab2  2802  rexrab2  2804  cbvrabcsf  3015  dfin5  3028  dfdif2  3029  ss2rab  3120  rabss  3121  ssrab  3122  rabss2  3127  ssrab2  3129  rabssab  3131  notab  3293  unrab  3294  inrab  3295  inrab2  3296  difrab  3297  dfrab2  3298  dfrab3  3299  notrab  3300  rabun2  3302  dfnul3  3313  rabn0r  3336  rabn0m  3337  rab0  3338  rabeq0  3339  dfif6  3423  rabsn  3537  reusn  3541  rabsneu  3543  elunirab  3696  elintrab  3730  ssintrab  3741  iunrab  3807  iinrabm  3822  intexrabim  4018  repizf2  4026  exss  4087  rabxp  4514  exse2  4849  mptpreima  4968  fndmin  5459  fncnvima2  5473  riotauni  5668  riotacl2  5675  snriota  5691  xp2  6001  unielxp  6002  dfopab2  6017  unfiexmid  6735  nnzrab  8930  nn0zrab  8931  shftlem  10429  shftuz  10430  shftdm  10435  negfi  10838  cnblcld  12457  bdcrab  12631