Definition df-rab 2462

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 2457	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1352	. . . . 5 class 𝑥
6	5, 3	wcel 2146	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2161	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1353	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  2650  rabid2  2651  rabbi  2652  rabswap  2653  nfrab1  2654  nfrabxy  2655  rabbiia  2720  rabbidva2  2722  rabeqf  2725  cbvrab  2733  rabab  2756  elrabi  2888  elrabf  2889  elrab3t  2890  ralrab2  2900  rexrab2  2902  cbvrabcsf  3120  dfin5  3134  dfdif2  3135  ss2rab  3229  rabss  3230  ssrab  3231  rabss2  3236  ssrab2  3238  rabssab  3241  notab  3403  unrab  3404  inrab  3405  inrab2  3406  difrab  3407  dfrab2  3408  dfrab3  3409  notrab  3410  rabun2  3412  dfnul3  3423  rabn0r  3447  rabn0m  3448  rab0  3449  rabeq0  3450  dfif6  3534  rabsn  3656  reusn  3660  rabsneu  3662  elunirab  3818  elintrab  3852  ssintrab  3863  iunrab  3929  iinrabm  3944  intexrabim  4148  repizf2  4157  exss  4221  rabxp  4657  exse2  4995  mptpreima  5114  fndmin  5615  fncnvima2  5629  riotauni  5827  riotacl2  5834  snriota  5850  xp2  6164  unielxp  6165  dfopab2  6180  unfiexmid  6907  nnzrab  9248  nn0zrab  9249  shftlem  10791  shftuz  10792  shftdm  10797  negfi  11202  cnblcld  13586  if0ab  14097  bdcrab  14144