Definition df-rab 2357

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 2352	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1283	. . . . 5 class 𝑥
6	5, 3	wcel 1433	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 102	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2067	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1284	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2529  rabid2  2530  rabbi  2531  rabswap  2532  nfrab1  2533  nfrabxy  2534  rabbiia  2591  rabeqf  2594  cbvrab  2599  rabab  2620  elrabi  2746  elrabf  2747  elrab3t  2748  ralrab2  2757  rexrab2  2759  cbvrabcsf  2967  dfin5  2980  dfdif2  2981  ss2rab  3070  rabss  3071  ssrab  3072  rabss2  3077  ssrab2  3079  rabssab  3081  notab  3234  unrab  3235  inrab  3236  inrab2  3237  difrab  3238  dfrab2  3239  dfrab3  3240  notrab  3241  rabun2  3243  dfnul3  3254  rabn0r  3271  rabn0m  3272  rab0  3273  rabeq0  3274  dfif6  3353  rabsn  3459  reusn  3463  rabsneu  3465  elunirab  3614  elintrab  3648  ssintrab  3659  iunrab  3725  iinrabm  3740  intexrabim  3928  repizf2  3936  exss  3982  rabxp  4398  exse2  4719  mptpreima  4834  fndmin  5295  fncnvima2  5309  riotauni  5494  riotacl2  5501  snriota  5517  xp2  5819  unielxp  5820  dfopab2  5835  nnzrab  8375  nn0zrab  8376  shftlem  9704  shftuz  9705  shftdm  9710  negfi  10110  bdcrab  10643