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	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		wph	|- ph
3	2 0 1	crab	|- { x e. A | ph }
4	0	cv	|- x
5	4 1	wcel	|- x e. A
6	5 2	wa	|- ( x e. A /\ ph )
7	6 0	cab	|- { x | ( x e. A /\ ph ) }
8	3 7	wceq	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }