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  3900  elintrab  3934  ssintrab  3945  iunrab  4012  iinrabm  4027  intexrabim  4236  repizf2  4245  exss  4312  rabxp  4755  exse2  5101  mptpreima  5221  fndmin  5741  fncnvima2  5755  riotauni  5960  riotacl2  5968  snriota  5985  xp2  6317  unielxp  6318  dfopab2  6333  unfiexmid  7076  nnzrab  9466  nn0zrab  9467  wrdnval  11097  shftlem  11322  shftuz  11323  shftdm  11328  negfi  11734  eqglact  13757  dfrhm2  14112  cnblcld  15203  2lgslem1b  15762  if0ab  16127  bdcrab  16173