Definition df-rab 2453

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 2448	. 2 class { x e. A | ph }
5	2	cv 1342	. . . . 5 class x
6	5, 3	wcel 2136	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2151	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1343	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2641  rabid2  2642  rabbi  2643  rabswap  2644  nfrab1  2645  nfrabxy  2646  rabbiia  2711  rabbidva2  2713  rabeqf  2716  cbvrab  2724  rabab  2747  elrabi  2879  elrabf  2880  elrab3t  2881  ralrab2  2891  rexrab2  2893  cbvrabcsf  3110  dfin5  3123  dfdif2  3124  ss2rab  3218  rabss  3219  ssrab  3220  rabss2  3225  ssrab2  3227  rabssab  3230  notab  3392  unrab  3393  inrab  3394  inrab2  3395  difrab  3396  dfrab2  3397  dfrab3  3398  notrab  3399  rabun2  3401  dfnul3  3412  rabn0r  3435  rabn0m  3436  rab0  3437  rabeq0  3438  dfif6  3522  rabsn  3643  reusn  3647  rabsneu  3649  elunirab  3802  elintrab  3836  ssintrab  3847  iunrab  3913  iinrabm  3928  intexrabim  4132  repizf2  4141  exss  4205  rabxp  4641  exse2  4978  mptpreima  5097  fndmin  5592  fncnvima2  5606  riotauni  5804  riotacl2  5811  snriota  5827  xp2  6141  unielxp  6142  dfopab2  6157  unfiexmid  6883  nnzrab  9215  nn0zrab  9216  shftlem  10758  shftuz  10759  shftdm  10764  negfi  11169  cnblcld  13175  if0ab  13687  bdcrab  13734