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  4289  repizf2  4299  exss  4367  rabxp  4812  exse2  5161  mptpreima  5281  fndmin  5816  fncnvima2  5830  riotauni  6045  riotacl2  6053  snriota  6070  xp2  6407  unielxp  6408  dfopab2  6423  ressuppss  6494  unfiexmid  7225  nnzrab  9668  nn0zrab  9669  wrdnval  11335  shftlem  11581  shftuz  11582  shftdm  11587  negfi  11994  eqglact  14028  dfrhm2  14461  cnblcld  15636  2lgslem1b  16208  vtxdfifiun  16538  bdcrab  16878