Definition df-rab 2537

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 2532	. 2 class { x e. A | ph }
5	2	cv 1401	. . . . 5 class x
6	5, 3	wcel 2209	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2224	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1402	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is used by:  rabid  2727  rabid2  2729  rabbi  2730  rabswap  2731  nfrab1  2732  nfrabw  2733  rabbidva2  2805  rabbiia  2807  rabeqf  2811  cbvrab  2819  rabab  2843  elrabi  2979  elrabf  2980  elrab3t  2981  ralrab2  2991  rexrab2  2993  cbvrabcsf  3213  dfin5  3227  dfdif2  3228  ss2rab  3324  rabss  3325  ssrab  3326  rabss2  3331  ssrab2  3333  rabssab  3337  notab  3503  unrab  3504  inrab  3505  inrab2  3506  difrab  3507  dfrab2  3508  dfrab3  3509  notrab  3510  rabun2  3512  dfnul3  3524  rabn0r  3548  rabn0m  3549  rab0  3551  rabeq0  3552  dfif6  3640  rabsn  3776  rabsnifsb  3777  reusn  3782  rabsneu  3784  elunirab  3948  elintrab  3982  ssintrab  3993  iunrab  4060  iinrabm  4075  intexrabim  4291  repizf2  4301  exss  4369  rabxp  4814  exse2  5164  mptpreima  5284  fndmin  5819  fncnvima2  5833  riotauni  6048  riotacl2  6056  snriota  6073  xp2  6411  unielxp  6412  dfopab2  6427  ressuppss  6498  unfiexmid  7229  nnzrab  9679  nn0zrab  9680  wrdnval  11357  shftlem  11603  shftuz  11604  shftdm  11609  negfi  12017  eqglact  14087  dfrhm2  14570  cnblcld  15761  2lgslem1b  16413  vtxdfifiun  16743  bdcrab  17083