Definition df-rab 2519

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 2514	. 2 class { x e. A | ph }
5	2	cv 1396	. . . . 5 class x
6	5, 3	wcel 2202	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2217	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1397	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2709  rabid2  2710  rabbi  2711  rabswap  2712  nfrab1  2713  nfrabw  2714  rabbidva2  2786  rabbiia  2788  rabeqf  2792  cbvrab  2800  rabab  2824  elrabi  2959  elrabf  2960  elrab3t  2961  ralrab2  2971  rexrab2  2973  cbvrabcsf  3193  dfin5  3207  dfdif2  3208  ss2rab  3303  rabss  3304  ssrab  3305  rabss2  3310  ssrab2  3312  rabssab  3315  notab  3477  unrab  3478  inrab  3479  inrab2  3480  difrab  3481  dfrab2  3482  dfrab3  3483  notrab  3484  rabun2  3486  dfnul3  3497  rabn0r  3521  rabn0m  3522  rab0  3523  rabeq0  3524  dfif6  3607  rabsn  3736  rabsnifsb  3737  reusn  3742  rabsneu  3744  elunirab  3906  elintrab  3940  ssintrab  3951  iunrab  4018  iinrabm  4033  intexrabim  4243  repizf2  4252  exss  4319  rabxp  4763  exse2  5110  mptpreima  5230  fndmin  5754  fncnvima2  5768  riotauni  5978  riotacl2  5986  snriota  6003  xp2  6336  unielxp  6337  dfopab2  6352  unfiexmid  7110  nnzrab  9503  nn0zrab  9504  wrdnval  11148  shftlem  11394  shftuz  11395  shftdm  11400  negfi  11806  eqglact  13830  dfrhm2  14187  cnblcld  15278  2lgslem1b  15837  vtxdfifiun  16167  if0ab  16452  bdcrab  16498