# Metamath Proof Explorer

## 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 ${setvar}{x}$
1 cA ${class}{A}$
2 wph ${wff}{\phi }$
3 2 0 1 crab ${class}\left\{{x}\in {A}|{\phi }\right\}$
4 0 cv ${setvar}{x}$
5 4 1 wcel ${wff}{x}\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\}$