Definition df-rab 2477

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 2472	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1363	. . . . 5 class 𝑥
6	5, 3	wcel 2160	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2175	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1364	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2666  rabid2  2667  rabbi  2668  rabswap  2669  nfrab1  2670  nfrabxy  2671  rabbiia  2737  rabbidva2  2739  rabeqf  2742  cbvrab  2750  rabab  2773  elrabi  2905  elrabf  2906  elrab3t  2907  ralrab2  2917  rexrab2  2919  cbvrabcsf  3137  dfin5  3151  dfdif2  3152  ss2rab  3246  rabss  3247  ssrab  3248  rabss2  3253  ssrab2  3255  rabssab  3258  notab  3420  unrab  3421  inrab  3422  inrab2  3423  difrab  3424  dfrab2  3425  dfrab3  3426  notrab  3427  rabun2  3429  dfnul3  3440  rabn0r  3464  rabn0m  3465  rab0  3466  rabeq0  3467  dfif6  3551  rabsn  3674  reusn  3678  rabsneu  3680  elunirab  3837  elintrab  3871  ssintrab  3882  iunrab  3949  iinrabm  3964  intexrabim  4171  repizf2  4180  exss  4245  rabxp  4681  exse2  5020  mptpreima  5140  fndmin  5644  fncnvima2  5658  riotauni  5859  riotacl2  5866  snriota  5882  xp2  6199  unielxp  6200  dfopab2  6215  unfiexmid  6947  nnzrab  9308  nn0zrab  9309  shftlem  10860  shftuz  10861  shftdm  10866  negfi  11271  eqglact  13181  dfrhm2  13521  cnblcld  14512  if0ab  15035  bdcrab  15082