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	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		wph	⊢ 𝜑
3	2 0 1	crab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 }
4	0	cv	⊢ 𝑥
5	4 1	wcel	⊢ 𝑥 ∈ 𝐴
6	5 2	wa	⊢ ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
7	6 0	cab	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
8	3 7	wceq	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }