Definition df-rab 2457

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 2452	. 2 class { x e. A | ph }
5	2	cv 1347	. . . . 5 class x
6	5, 3	wcel 2141	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2156	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1348	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2645  rabid2  2646  rabbi  2647  rabswap  2648  nfrab1  2649  nfrabxy  2650  rabbiia  2715  rabbidva2  2717  rabeqf  2720  cbvrab  2728  rabab  2751  elrabi  2883  elrabf  2884  elrab3t  2885  ralrab2  2895  rexrab2  2897  cbvrabcsf  3114  dfin5  3128  dfdif2  3129  ss2rab  3223  rabss  3224  ssrab  3225  rabss2  3230  ssrab2  3232  rabssab  3235  notab  3397  unrab  3398  inrab  3399  inrab2  3400  difrab  3401  dfrab2  3402  dfrab3  3403  notrab  3404  rabun2  3406  dfnul3  3417  rabn0r  3441  rabn0m  3442  rab0  3443  rabeq0  3444  dfif6  3528  rabsn  3650  reusn  3654  rabsneu  3656  elunirab  3809  elintrab  3843  ssintrab  3854  iunrab  3920  iinrabm  3935  intexrabim  4139  repizf2  4148  exss  4212  rabxp  4648  exse2  4985  mptpreima  5104  fndmin  5603  fncnvima2  5617  riotauni  5815  riotacl2  5822  snriota  5838  xp2  6152  unielxp  6153  dfopab2  6168  unfiexmid  6895  nnzrab  9236  nn0zrab  9237  shftlem  10780  shftuz  10781  shftdm  10786  negfi  11191  cnblcld  13329  if0ab  13840  bdcrab  13887