Definition df-rab 2494

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 2489	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1372	. . . . 5 class 𝑥
6	5, 3	wcel 2177	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2192	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1373	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2683  rabid2  2684  rabbi  2685  rabswap  2686  nfrab1  2687  nfrabw  2688  rabbiia  2758  rabbidva2  2760  rabeqf  2763  cbvrab  2771  rabab  2794  elrabi  2927  elrabf  2928  elrab3t  2929  ralrab2  2939  rexrab2  2941  cbvrabcsf  3160  dfin5  3174  dfdif2  3175  ss2rab  3270  rabss  3271  ssrab  3272  rabss2  3277  ssrab2  3279  rabssab  3282  notab  3444  unrab  3445  inrab  3446  inrab2  3447  difrab  3448  dfrab2  3449  dfrab3  3450  notrab  3451  rabun2  3453  dfnul3  3464  rabn0r  3488  rabn0m  3489  rab0  3490  rabeq0  3491  dfif6  3574  rabsn  3701  reusn  3705  rabsneu  3707  elunirab  3865  elintrab  3899  ssintrab  3910  iunrab  3977  iinrabm  3992  intexrabim  4201  repizf2  4210  exss  4275  rabxp  4716  exse2  5061  mptpreima  5181  fndmin  5694  fncnvima2  5708  riotauni  5913  riotacl2  5920  snriota  5936  xp2  6266  unielxp  6267  dfopab2  6282  unfiexmid  7022  nnzrab  9403  nn0zrab  9404  wrdnval  11031  shftlem  11171  shftuz  11172  shftdm  11177  negfi  11583  eqglact  13605  dfrhm2  13960  cnblcld  15051  2lgslem1b  15610  if0ab  15815  bdcrab  15862