Definition df-rab 2519

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 2514	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1396	. . . . 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 1397	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2709  rabid2  2710  rabbi  2711  rabswap  2712  nfrab1  2713  nfrabw  2714  rabbidva2  2786  rabbiia  2788  rabeqf  2792  cbvrab  2800  rabab  2824  elrabi  2959  elrabf  2960  elrab3t  2961  ralrab2  2971  rexrab2  2973  cbvrabcsf  3193  dfin5  3207  dfdif2  3208  ss2rab  3303  rabss  3304  ssrab  3305  rabss2  3310  ssrab2  3312  rabssab  3315  notab  3477  unrab  3478  inrab  3479  inrab2  3480  difrab  3481  dfrab2  3482  dfrab3  3483  notrab  3484  rabun2  3486  dfnul3  3497  rabn0r  3521  rabn0m  3522  rab0  3523  rabeq0  3524  dfif6  3607  rabsn  3736  rabsnifsb  3737  reusn  3742  rabsneu  3744  elunirab  3906  elintrab  3940  ssintrab  3951  iunrab  4018  iinrabm  4033  intexrabim  4243  repizf2  4252  exss  4319  rabxp  4763  exse2  5110  mptpreima  5230  fndmin  5754  fncnvima2  5768  riotauni  5977  riotacl2  5985  snriota  6002  xp2  6335  unielxp  6336  dfopab2  6351  unfiexmid  7109  nnzrab  9502  nn0zrab  9503  wrdnval  11143  shftlem  11376  shftuz  11377  shftdm  11382  negfi  11788  eqglact  13811  dfrhm2  14167  cnblcld  15258  2lgslem1b  15817  vtxdfifiun  16147  if0ab  16401  bdcrab  16447