Definition df-wl-rab

Description: Define a restricted class abstraction (class builder), which is the class of all x in A such that ph is true. Definition of TakeutiZaring p. 20. (Contributed by NM, 22-Nov-1994) Isolate x from A. (Revised by Wolf Lammen, 28-May-2023)

	Ref	Expression
Assertion	df-wl-rab	$$⊢\left\{x:A|\phi \right\}=\left\{y|\left(y\in A\wedge \forall x\left(x=y\to \phi \right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	wl-crab	$$class\left\{x:A|\phi \right\}$$
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	5 1	wcel	$$wffy\in A$$
7	0	cv	$$setvarx$$
8	7 5	wceq	$$wffx=y$$
9	8 2	wi	$$wff\left(x=y\to \phi \right)$$
10	9 0	wal	$$wff\forall x\left(x=y\to \phi \right)$$
11	6 10	wa	$$wff\left(y\in A\wedge \forall x\left(x=y\to \phi \right)\right)$$
12	11 4	cab	$$class\left\{y|\left(y\in A\wedge \forall x\left(x=y\to \phi \right)\right)\right\}$$
13	3 12	wceq	$$wff\left\{x:A|\phi \right\}=\left\{y|\left(y\in A\wedge \forall x\left(x=y\to \phi \right)\right)\right\}$$