Definition df-rab 2315

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 2310	. 2 class { x e. A | ph }
5	2	cv 1242	. . . . 5 class x
6	5, 3	wcel 1393	. . . 4 wff x e. A
7	6, 1	wa 97	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2026	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1243	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2485  rabid2  2486  rabbi  2487  rabswap  2488  nfrab1  2489  nfrabxy  2490  rabbiia  2547  rabeqf  2550  cbvrab  2555  rabab  2575  elrabi  2695  elrabf  2696  elrab3t  2697  ralrab2  2706  rexrab2  2708  cbvrabcsf  2911  dfin5  2925  dfdif2  2926  ss2rab  3016  rabss  3017  ssrab  3018  rabss2  3023  ssrab2  3025  rabssab  3027  notab  3207  unrab  3208  inrab  3209  inrab2  3210  difrab  3211  dfrab2  3212  dfrab3  3213  notrab  3214  rabun2  3216  dfnul3  3227  rabn0r  3244  rabn0m  3245  rab0  3246  rabeq0  3247  dfif6  3333  rabsn  3437  reusn  3441  rabsneu  3443  elunirab  3593  elintrab  3627  ssintrab  3638  iunrab  3704  iinrabm  3719  intexrabim  3907  repizf2  3915  exss  3963  rabxp  4380  exse2  4699  mptpreima  4814  fndmin  5274  fncnvima2  5288  riotauni  5474  riotacl2  5481  snriota  5497  xp2  5799  unielxp  5800  dfopab2  5815  nnzrab  8269  nn0zrab  8270  shftlem  9417  shftuz  9418  shftdm  9423  bdcrab  9972