![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-rab | Structured version Visualization version GIF version |
Description: Define a restricted class
abstraction (class builder), which is the class
of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of
[TakeutiZaring] p. 20.
Note: For the reading given above Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather get a class of all those 𝑥 fulfilling 𝜑 that happen to be contained in the corresponding 𝐴(𝑥). This need not be a subset of any of the 𝐴(𝑥) at all. Such interpretation is rarely needed (see also df-ral 3112). (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
df-rab | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cA | . . 3 class 𝐴 | |
4 | 1, 2, 3 | crab 3111 | . 2 class {𝑥 ∈ 𝐴 ∣ 𝜑} |
5 | 2 | cv 1524 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2083 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 396 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cab 2777 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
9 | 4, 8 | wceq 1525 | 1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
Copyright terms: Public domain | W3C validator |