Definition df-rab 2362

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 2357	. 2 class { x e. A | ph }
5	2	cv 1284	. . . . 5 class x
6	5, 3	wcel 1434	. . . 4 wff x e. A
7	6, 1	wa 102	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2069	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1285	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2534  rabid2  2535  rabbi  2536  rabswap  2537  nfrab1  2538  nfrabxy  2539  rabbiia  2596  rabeqf  2600  cbvrab  2608  rabab  2629  elrabi  2754  elrabf  2755  elrab3t  2756  ralrab2  2766  rexrab2  2768  cbvrabcsf  2976  dfin5  2989  dfdif2  2990  ss2rab  3079  rabss  3080  ssrab  3081  rabss2  3086  ssrab2  3088  rabssab  3090  notab  3250  unrab  3251  inrab  3252  inrab2  3253  difrab  3254  dfrab2  3255  dfrab3  3256  notrab  3257  rabun2  3259  dfnul3  3270  rabn0r  3287  rabn0m  3288  rab0  3289  rabeq0  3290  dfif6  3370  rabsn  3477  reusn  3481  rabsneu  3483  elunirab  3634  elintrab  3668  ssintrab  3679  iunrab  3745  iinrabm  3760  intexrabim  3948  repizf2  3956  exss  4010  rabxp  4426  exse2  4749  mptpreima  4864  fndmin  5326  fncnvima2  5340  riotauni  5525  riotacl2  5532  snriota  5548  xp2  5850  unielxp  5851  dfopab2  5866  unfiexmid  6462  nnzrab  8508  nn0zrab  8509  shftlem  9905  shftuz  9906  shftdm  9911  negfi  10311  bdcrab  10910