Definition df-rab 2517

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 2512	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1394	. . . . 5 class 𝑥
6	5, 3	wcel 2200	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2215	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1395	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2707  rabid2  2708  rabbi  2709  rabswap  2710  nfrab1  2711  nfrabw  2712  rabbidva2  2784  rabbiia  2786  rabeqf  2790  cbvrab  2798  rabab  2822  elrabi  2957  elrabf  2958  elrab3t  2959  ralrab2  2969  rexrab2  2971  cbvrabcsf  3191  dfin5  3205  dfdif2  3206  ss2rab  3301  rabss  3302  ssrab  3303  rabss2  3308  ssrab2  3310  rabssab  3313  notab  3475  unrab  3476  inrab  3477  inrab2  3478  difrab  3479  dfrab2  3480  dfrab3  3481  notrab  3482  rabun2  3484  dfnul3  3495  rabn0r  3519  rabn0m  3520  rab0  3521  rabeq0  3522  dfif6  3605  rabsn  3734  reusn  3738  rabsneu  3740  elunirab  3902  elintrab  3936  ssintrab  3947  iunrab  4014  iinrabm  4029  intexrabim  4239  repizf2  4248  exss  4315  rabxp  4759  exse2  5106  mptpreima  5226  fndmin  5748  fncnvima2  5762  riotauni  5971  riotacl2  5979  snriota  5996  xp2  6329  unielxp  6330  dfopab2  6345  unfiexmid  7101  nnzrab  9491  nn0zrab  9492  wrdnval  11131  shftlem  11364  shftuz  11365  shftdm  11370  negfi  11776  eqglact  13799  dfrhm2  14155  cnblcld  15246  2lgslem1b  15805  vtxdfifiun  16099  if0ab  16311  bdcrab  16357