Definition df-rab 2481

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 2476	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1363	. . . . 5 class 𝑥
6	5, 3	wcel 2164	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2179	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1364	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2670  rabid2  2671  rabbi  2672  rabswap  2673  nfrab1  2674  nfrabw  2675  rabbiia  2745  rabbidva2  2747  rabeqf  2750  cbvrab  2758  rabab  2781  elrabi  2914  elrabf  2915  elrab3t  2916  ralrab2  2926  rexrab2  2928  cbvrabcsf  3147  dfin5  3161  dfdif2  3162  ss2rab  3256  rabss  3257  ssrab  3258  rabss2  3263  ssrab2  3265  rabssab  3268  notab  3430  unrab  3431  inrab  3432  inrab2  3433  difrab  3434  dfrab2  3435  dfrab3  3436  notrab  3437  rabun2  3439  dfnul3  3450  rabn0r  3474  rabn0m  3475  rab0  3476  rabeq0  3477  dfif6  3560  rabsn  3686  reusn  3690  rabsneu  3692  elunirab  3849  elintrab  3883  ssintrab  3894  iunrab  3961  iinrabm  3976  intexrabim  4183  repizf2  4192  exss  4257  rabxp  4697  exse2  5040  mptpreima  5160  fndmin  5666  fncnvima2  5680  riotauni  5881  riotacl2  5888  snriota  5904  xp2  6228  unielxp  6229  dfopab2  6244  unfiexmid  6976  nnzrab  9344  nn0zrab  9345  wrdnval  10947  shftlem  10963  shftuz  10964  shftdm  10969  negfi  11374  eqglact  13298  dfrhm2  13653  cnblcld  14714  2lgslem1b  15246  if0ab  15367  bdcrab  15414