Definition df-rab 2484

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 2479	. 2 class { x e. A | ph }
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2167	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2182	. 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  2673  rabid2  2674  rabbi  2675  rabswap  2676  nfrab1  2677  nfrabw  2678  rabbiia  2748  rabbidva2  2750  rabeqf  2753  cbvrab  2761  rabab  2784  elrabi  2917  elrabf  2918  elrab3t  2919  ralrab2  2929  rexrab2  2931  cbvrabcsf  3150  dfin5  3164  dfdif2  3165  ss2rab  3259  rabss  3260  ssrab  3261  rabss2  3266  ssrab2  3268  rabssab  3271  notab  3433  unrab  3434  inrab  3435  inrab2  3436  difrab  3437  dfrab2  3438  dfrab3  3439  notrab  3440  rabun2  3442  dfnul3  3453  rabn0r  3477  rabn0m  3478  rab0  3479  rabeq0  3480  dfif6  3563  rabsn  3689  reusn  3693  rabsneu  3695  elunirab  3852  elintrab  3886  ssintrab  3897  iunrab  3964  iinrabm  3979  intexrabim  4186  repizf2  4195  exss  4260  rabxp  4700  exse2  5043  mptpreima  5163  fndmin  5669  fncnvima2  5683  riotauni  5884  riotacl2  5891  snriota  5907  xp2  6231  unielxp  6232  dfopab2  6247  unfiexmid  6979  nnzrab  9350  nn0zrab  9351  wrdnval  10965  shftlem  10981  shftuz  10982  shftdm  10987  negfi  11393  eqglact  13355  dfrhm2  13710  cnblcld  14771  2lgslem1b  15330  if0ab  15451  bdcrab  15498