Definition df-rab 2477

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

This definition is referenced by:  rabid  2666  rabid2  2667  rabbi  2668  rabswap  2669  nfrab1  2670  nfrabxy  2671  rabbiia  2737  rabbidva2  2739  rabeqf  2742  cbvrab  2750  rabab  2773  elrabi  2905  elrabf  2906  elrab3t  2907  ralrab2  2917  rexrab2  2919  cbvrabcsf  3137  dfin5  3151  dfdif2  3152  ss2rab  3246  rabss  3247  ssrab  3248  rabss2  3253  ssrab2  3255  rabssab  3258  notab  3420  unrab  3421  inrab  3422  inrab2  3423  difrab  3424  dfrab2  3425  dfrab3  3426  notrab  3427  rabun2  3429  dfnul3  3440  rabn0r  3464  rabn0m  3465  rab0  3466  rabeq0  3467  dfif6  3551  rabsn  3674  reusn  3678  rabsneu  3680  elunirab  3837  elintrab  3871  ssintrab  3882  iunrab  3949  iinrabm  3964  intexrabim  4168  repizf2  4177  exss  4242  rabxp  4678  exse2  5017  mptpreima  5137  fndmin  5640  fncnvima2  5654  riotauni  5854  riotacl2  5861  snriota  5877  xp2  6193  unielxp  6194  dfopab2  6209  unfiexmid  6941  nnzrab  9302  nn0zrab  9303  shftlem  10852  shftuz  10853  shftdm  10858  negfi  11263  eqglact  13157  dfrhm2  13497  cnblcld  14472  if0ab  14995  bdcrab  15042