Definition df-rab 2537

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 2532	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1401	. . . . 5 class 𝑥
6	5, 3	wcel 2209	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2224	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1402	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2727  rabid2  2729  rabbi  2730  rabswap  2731  nfrab1  2732  nfrabw  2733  rabbidva2  2805  rabbiia  2807  rabeqf  2811  cbvrab  2819  rabab  2843  elrabi  2979  elrabf  2980  elrab3t  2981  ralrab2  2991  rexrab2  2993  cbvrabcsf  3213  dfin5  3227  dfdif2  3228  ss2rab  3324  rabss  3325  ssrab  3326  rabss2  3331  ssrab2  3333  rabssab  3337  notab  3503  unrab  3504  inrab  3505  inrab2  3506  difrab  3507  dfrab2  3508  dfrab3  3509  notrab  3510  rabun2  3512  dfnul3  3524  rabn0r  3548  rabn0m  3549  rab0  3551  rabeq0  3552  dfif6  3640  rabsn  3775  rabsnifsb  3776  reusn  3781  rabsneu  3783  elunirab  3946  elintrab  3980  ssintrab  3991  iunrab  4058  iinrabm  4073  intexrabim  4287  repizf2  4297  exss  4365  rabxp  4810  exse2  5159  mptpreima  5279  fndmin  5810  fncnvima2  5824  riotauni  6038  riotacl2  6046  snriota  6063  xp2  6400  unielxp  6401  dfopab2  6416  ressuppss  6487  unfiexmid  7218  nnzrab  9650  nn0zrab  9651  wrdnval  11316  shftlem  11562  shftuz  11563  shftdm  11568  negfi  11975  eqglact  14008  dfrhm2  14437  cnblcld  15562  2lgslem1b  16125  vtxdfifiun  16455  bdcrab  16795