Definition df-rab 2497

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 2492	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1374	. . . . 5 class 𝑥
6	5, 3	wcel 2180	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2195	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1375	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2687  rabid2  2688  rabbi  2689  rabswap  2690  nfrab1  2691  nfrabw  2692  rabbiia  2764  rabbidva2  2766  rabeqf  2769  cbvrab  2777  rabab  2801  elrabi  2936  elrabf  2937  elrab3t  2938  ralrab2  2948  rexrab2  2950  cbvrabcsf  3170  dfin5  3184  dfdif2  3185  ss2rab  3280  rabss  3281  ssrab  3282  rabss2  3287  ssrab2  3289  rabssab  3292  notab  3454  unrab  3455  inrab  3456  inrab2  3457  difrab  3458  dfrab2  3459  dfrab3  3460  notrab  3461  rabun2  3463  dfnul3  3474  rabn0r  3498  rabn0m  3499  rab0  3500  rabeq0  3501  dfif6  3584  rabsn  3713  reusn  3717  rabsneu  3719  elunirab  3880  elintrab  3914  ssintrab  3925  iunrab  3992  iinrabm  4007  intexrabim  4216  repizf2  4225  exss  4292  rabxp  4733  exse2  5078  mptpreima  5198  fndmin  5715  fncnvima2  5729  riotauni  5934  riotacl2  5942  snriota  5959  xp2  6289  unielxp  6290  dfopab2  6305  unfiexmid  7048  nnzrab  9438  nn0zrab  9439  wrdnval  11068  shftlem  11293  shftuz  11294  shftdm  11299  negfi  11705  eqglact  13728  dfrhm2  14083  cnblcld  15174  2lgslem1b  15733  if0ab  16079  bdcrab  16125