Definition df-rab 2531

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 2526	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1397	. . . . 5 class 𝑥
6	5, 3	wcel 2205	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2220	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1398	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2721  rabid2  2723  rabbi  2724  rabswap  2725  nfrab1  2726  nfrabw  2727  rabbidva2  2799  rabbiia  2801  rabeqf  2805  cbvrab  2813  rabab  2837  elrabi  2973  elrabf  2974  elrab3t  2975  ralrab2  2985  rexrab2  2987  cbvrabcsf  3207  dfin5  3221  dfdif2  3222  ss2rab  3318  rabss  3319  ssrab  3320  rabss2  3325  ssrab2  3327  rabssab  3331  notab  3495  unrab  3496  inrab  3497  inrab2  3498  difrab  3499  dfrab2  3500  dfrab3  3501  notrab  3502  rabun2  3504  dfnul3  3515  rabn0r  3539  rabn0m  3540  rab0  3541  rabeq0  3542  dfif6  3626  rabsn  3761  rabsnifsb  3762  reusn  3767  rabsneu  3769  elunirab  3932  elintrab  3966  ssintrab  3977  iunrab  4044  iinrabm  4059  intexrabim  4270  repizf2  4280  exss  4348  rabxp  4792  exse2  5141  mptpreima  5261  fndmin  5790  fncnvima2  5804  riotauni  6018  riotacl2  6026  snriota  6043  xp2  6380  unielxp  6381  dfopab2  6396  ressuppss  6467  unfiexmid  7191  nnzrab  9618  nn0zrab  9619  wrdnval  11280  shftlem  11526  shftuz  11527  shftdm  11532  negfi  11938  eqglact  13978  dfrhm2  14399  cnblcld  15526  2lgslem1b  16088  vtxdfifiun  16418  bdcrab  16748