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.
Note: For the reading given above F/_ x A is required, though, for example, asserted when x and A are disjoint.
Should instead A depend on x , you rather get a class of all those x fulfilling ph that happen to be contained in the corresponding A ( x ) . This need not be a subset of any of the A ( x ) at all. Such interpretation is rarely needed (see also df-ral ). (Contributed by NM, 22-Nov-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
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 | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |