Definition df-rab 2481

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 2476	. 2 class { x e. A | ph }
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2164	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2179	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1364	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2670  rabid2  2671  rabbi  2672  rabswap  2673  nfrab1  2674  nfrabw  2675  rabbiia  2745  rabbidva2  2747  rabeqf  2750  cbvrab  2758  rabab  2781  elrabi  2913  elrabf  2914  elrab3t  2915  ralrab2  2925  rexrab2  2927  cbvrabcsf  3146  dfin5  3160  dfdif2  3161  ss2rab  3255  rabss  3256  ssrab  3257  rabss2  3262  ssrab2  3264  rabssab  3267  notab  3429  unrab  3430  inrab  3431  inrab2  3432  difrab  3433  dfrab2  3434  dfrab3  3435  notrab  3436  rabun2  3438  dfnul3  3449  rabn0r  3473  rabn0m  3474  rab0  3475  rabeq0  3476  dfif6  3559  rabsn  3685  reusn  3689  rabsneu  3691  elunirab  3848  elintrab  3882  ssintrab  3893  iunrab  3960  iinrabm  3975  intexrabim  4182  repizf2  4191  exss  4256  rabxp  4696  exse2  5039  mptpreima  5159  fndmin  5665  fncnvima2  5679  riotauni  5880  riotacl2  5887  snriota  5903  xp2  6226  unielxp  6227  dfopab2  6242  unfiexmid  6974  nnzrab  9341  nn0zrab  9342  wrdnval  10944  shftlem  10960  shftuz  10961  shftdm  10966  negfi  11371  eqglact  13295  dfrhm2  13650  cnblcld  14703  if0ab  15297  bdcrab  15344