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  4710  exse2  5053  mptpreima  5173  fndmin  5681  fncnvima2  5695  riotauni  5896  riotacl2  5903  snriota  5919  xp2  6249  unielxp  6250  dfopab2  6265  unfiexmid  6997  nnzrab  9378  nn0zrab  9379  wrdnval  10999  shftlem  11046  shftuz  11047  shftdm  11052  negfi  11458  eqglact  13479  dfrhm2  13834  cnblcld  14925  2lgslem1b  15484  if0ab  15605  bdcrab  15652