Definition df-rab 2484

Description: Define a restricted class abstraction (class builder), which is the class of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
df-rab	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

Detailed syntax breakdown of Definition df-rab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	crab 2479	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1363	. . . . 5 class 𝑥
6	5, 3	wcel 2167	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2182	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1364	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2673  rabid2  2674  rabbi  2675  rabswap  2676  nfrab1  2677  nfrabw  2678  rabbiia  2748  rabbidva2  2750  rabeqf  2753  cbvrab  2761  rabab  2784  elrabi  2917  elrabf  2918  elrab3t  2919  ralrab2  2929  rexrab2  2931  cbvrabcsf  3150  dfin5  3164  dfdif2  3165  ss2rab  3260  rabss  3261  ssrab  3262  rabss2  3267  ssrab2  3269  rabssab  3272  notab  3434  unrab  3435  inrab  3436  inrab2  3437  difrab  3438  dfrab2  3439  dfrab3  3440  notrab  3441  rabun2  3443  dfnul3  3454  rabn0r  3478  rabn0m  3479  rab0  3480  rabeq0  3481  dfif6  3564  rabsn  3690  reusn  3694  rabsneu  3696  elunirab  3853  elintrab  3887  ssintrab  3898  iunrab  3965  iinrabm  3980  intexrabim  4187  repizf2  4196  exss  4261  rabxp  4701  exse2  5044  mptpreima  5164  fndmin  5672  fncnvima2  5686  riotauni  5887  riotacl2  5894  snriota  5910  xp2  6240  unielxp  6241  dfopab2  6256  unfiexmid  6988  nnzrab  9367  nn0zrab  9368  wrdnval  10982  shftlem  10998  shftuz  10999  shftdm  11004  negfi  11410  eqglact  13431  dfrhm2  13786  cnblcld  14855  2lgslem1b  15414  if0ab  15535  bdcrab  15582