Definition df-rab 2517

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 2512	. 2 class { x e. A | ph }
5	2	cv 1394	. . . . 5 class x
6	5, 3	wcel 2200	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2215	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1395	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2707  rabid2  2708  rabbi  2709  rabswap  2710  nfrab1  2711  nfrabw  2712  rabbidva2  2784  rabbiia  2786  rabeqf  2790  cbvrab  2798  rabab  2822  elrabi  2957  elrabf  2958  elrab3t  2959  ralrab2  2969  rexrab2  2971  cbvrabcsf  3191  dfin5  3205  dfdif2  3206  ss2rab  3301  rabss  3302  ssrab  3303  rabss2  3308  ssrab2  3310  rabssab  3313  notab  3475  unrab  3476  inrab  3477  inrab2  3478  difrab  3479  dfrab2  3480  dfrab3  3481  notrab  3482  rabun2  3484  dfnul3  3495  rabn0r  3519  rabn0m  3520  rab0  3521  rabeq0  3522  dfif6  3605  rabsn  3734  rabsnifsb  3735  reusn  3740  rabsneu  3742  elunirab  3904  elintrab  3938  ssintrab  3949  iunrab  4016  iinrabm  4031  intexrabim  4241  repizf2  4250  exss  4317  rabxp  4761  exse2  5108  mptpreima  5228  fndmin  5750  fncnvima2  5764  riotauni  5973  riotacl2  5981  snriota  5998  xp2  6331  unielxp  6332  dfopab2  6347  unfiexmid  7103  nnzrab  9493  nn0zrab  9494  wrdnval  11134  shftlem  11367  shftuz  11368  shftdm  11373  negfi  11779  eqglact  13802  dfrhm2  14158  cnblcld  15249  2lgslem1b  15808  vtxdfifiun  16103  if0ab  16337  bdcrab  16383