Definition df-rab 2364

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 2359	. 2 class { x e. A | ph }
5	2	cv 1286	. . . . 5 class x
6	5, 3	wcel 1436	. . . 4 wff x e. A
7	6, 1	wa 102	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2071	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1287	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2538  rabid2  2539  rabbi  2540  rabswap  2541  nfrab1  2542  nfrabxy  2543  rabbiia  2600  rabbidva2  2602  rabeqf  2605  cbvrab  2613  rabab  2634  elrabi  2759  elrabf  2760  elrab3t  2761  ralrab2  2771  rexrab2  2773  cbvrabcsf  2982  dfin5  2995  dfdif2  2996  ss2rab  3086  rabss  3087  ssrab  3088  rabss2  3093  ssrab2  3095  rabssab  3097  notab  3258  unrab  3259  inrab  3260  inrab2  3261  difrab  3262  dfrab2  3263  dfrab3  3264  notrab  3265  rabun2  3267  dfnul3  3278  rabn0r  3298  rabn0m  3299  rab0  3300  rabeq0  3301  dfif6  3381  rabsn  3494  reusn  3498  rabsneu  3500  elunirab  3651  elintrab  3685  ssintrab  3696  iunrab  3762  iinrabm  3777  intexrabim  3966  repizf2  3974  exss  4030  rabxp  4448  exse2  4775  mptpreima  4892  fndmin  5371  fncnvima2  5385  riotauni  5577  riotacl2  5584  snriota  5600  xp2  5902  unielxp  5903  dfopab2  5918  unfiexmid  6582  nnzrab  8710  nn0zrab  8711  shftlem  10150  shftuz  10151  shftdm  10156  negfi  10557  bdcrab  11212