Definition df-wl-rab 34896

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.) Isolate x from A. (Revised by Wolf Lammen, 28-May-2023.)

Assertion

Ref	Expression
df-wl-rab	⊢ {𝑥 : 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))}

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Detailed syntax breakdown of Definition df-wl-rab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wl-crab 34871	. 2 class {𝑥 : 𝐴 ∣ 𝜑}
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1535	. . . . 5 class 𝑦
7	6, 3	wcel 2113	. . . 4 wff 𝑦 ∈ 𝐴
8	2, 5	weq 1963	. . . . . 6 wff 𝑥 = 𝑦
9	8, 1	wi 4	. . . . 5 wff (𝑥 = 𝑦 → 𝜑)
10	9, 2	wal 1534	. . . 4 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
11	7, 10	wa 398	. . 3 wff (𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))
12	11, 5	cab 2798	. 2 class {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))}
13	4, 12	wceq 1536	1 wff {𝑥 : 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))}

This definition is referenced by:  wl-dfrabsb  34897