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  rabbiia  2784  rabbidva2  2786  rabeqf  2789  cbvrab  2797  rabab  2821  elrabi  2956  elrabf  2957  elrab3t  2958  ralrab2  2968  rexrab2  2970  cbvrabcsf  3190  dfin5  3204  dfdif2  3205  ss2rab  3300  rabss  3301  ssrab  3302  rabss2  3307  ssrab2  3309  rabssab  3312  notab  3474  unrab  3475  inrab  3476  inrab2  3477  difrab  3478  dfrab2  3479  dfrab3  3480  notrab  3481  rabun2  3483  dfnul3  3494  rabn0r  3518  rabn0m  3519  rab0  3520  rabeq0  3521  dfif6  3604  rabsn  3733  reusn  3737  rabsneu  3739  elunirab  3901  elintrab  3935  ssintrab  3946  iunrab  4013  iinrabm  4028  intexrabim  4237  repizf2  4246  exss  4313  rabxp  4756  exse2  5102  mptpreima  5222  fndmin  5744  fncnvima2  5758  riotauni  5967  riotacl2  5975  snriota  5992  xp2  6325  unielxp  6326  dfopab2  6341  unfiexmid  7091  nnzrab  9481  nn0zrab  9482  wrdnval  11115  shftlem  11342  shftuz  11343  shftdm  11348  negfi  11754  eqglact  13777  dfrhm2  14133  cnblcld  15224  2lgslem1b  15783  vtxdfifiun  16056  if0ab  16224  bdcrab  16270