Definition df-rab 2520

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

This definition is referenced by:  rabid  2710  rabid2  2711  rabbi  2712  rabswap  2713  nfrab1  2714  nfrabw  2715  rabbidva2  2787  rabbiia  2789  rabeqf  2793  cbvrab  2801  rabab  2825  elrabi  2960  elrabf  2961  elrab3t  2962  ralrab2  2972  rexrab2  2974  cbvrabcsf  3194  dfin5  3208  dfdif2  3209  ss2rab  3304  rabss  3305  ssrab  3306  rabss2  3311  ssrab2  3313  rabssab  3317  notab  3479  unrab  3480  inrab  3481  inrab2  3482  difrab  3483  dfrab2  3484  dfrab3  3485  notrab  3486  rabun2  3488  dfnul3  3499  rabn0r  3523  rabn0m  3524  rab0  3525  rabeq0  3526  dfif6  3609  rabsn  3740  rabsnifsb  3741  reusn  3746  rabsneu  3748  elunirab  3911  elintrab  3945  ssintrab  3956  iunrab  4023  iinrabm  4038  intexrabim  4248  repizf2  4258  exss  4325  rabxp  4769  exse2  5117  mptpreima  5237  fndmin  5763  fncnvima2  5777  riotauni  5988  riotacl2  5996  snriota  6013  xp2  6345  unielxp  6346  dfopab2  6361  ressuppss  6432  unfiexmid  7153  nnzrab  9564  nn0zrab  9565  wrdnval  11210  shftlem  11456  shftuz  11457  shftdm  11462  negfi  11868  eqglact  13892  dfrhm2  14249  cnblcld  15346  2lgslem1b  15908  vtxdfifiun  16238  bdcrab  16568