Definition df-rab

Description: Define a restricted class abstraction (class builder): { x e. A | ph } is the class of all sets x in A such that ph ( x ) is true. Definition of TakeutiZaring p. 20.

For the interpretation given in the previous paragraph to be correct, we need to assume F/_ x A , which is the case as soon as x and A are disjoint, which is generally the case. If A were to depend on x , then the interpretation would be less obvious (think of the two extreme cases A = { x } and A = x , for instance). See also df-ral . (Contributed by NM, 22-Nov-1994)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	crab	$$class\left\{x\in A|\phi \right\}$$
4	0	cv	$$setvarx$$
5	4 1	wcel	$$wffx\in A$$
6	5 2	wa	$$wff\left(x\in A\wedge \phi \right)$$
7	6 0	cab	$$class\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
8	3 7	wceq	$$wff\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$