Definition df-rab 2492

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 2487	. 2 class { x e. A | ph }
5	2	cv 1371	. . . . 5 class x
6	5, 3	wcel 2175	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2190	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1372	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2681  rabid2  2682  rabbi  2683  rabswap  2684  nfrab1  2685  nfrabw  2686  rabbiia  2756  rabbidva2  2758  rabeqf  2761  cbvrab  2769  rabab  2792  elrabi  2925  elrabf  2926  elrab3t  2927  ralrab2  2937  rexrab2  2939  cbvrabcsf  3158  dfin5  3172  dfdif2  3173  ss2rab  3268  rabss  3269  ssrab  3270  rabss2  3275  ssrab2  3277  rabssab  3280  notab  3442  unrab  3443  inrab  3444  inrab2  3445  difrab  3446  dfrab2  3447  dfrab3  3448  notrab  3449  rabun2  3451  dfnul3  3462  rabn0r  3486  rabn0m  3487  rab0  3488  rabeq0  3489  dfif6  3572  rabsn  3699  reusn  3703  rabsneu  3705  elunirab  3862  elintrab  3896  ssintrab  3907  iunrab  3974  iinrabm  3989  intexrabim  4196  repizf2  4205  exss  4270  rabxp  4711  exse2  5055  mptpreima  5175  fndmin  5686  fncnvima2  5700  riotauni  5905  riotacl2  5912  snriota  5928  xp2  6258  unielxp  6259  dfopab2  6274  unfiexmid  7014  nnzrab  9395  nn0zrab  9396  wrdnval  11022  shftlem  11069  shftuz  11070  shftdm  11075  negfi  11481  eqglact  13503  dfrhm2  13858  cnblcld  14949  2lgslem1b  15508  if0ab  15674  bdcrab  15721