Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-oprab | GIF version |
Description: Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 5745 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpo 5874. (Contributed by NM, 12-Mar-1995.) |
Ref | Expression |
---|---|
df-oprab | ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | vz | . . 3 setvar 𝑧 | |
5 | 1, 2, 3, 4 | coprab 5743 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
6 | vw | . . . . . . . . 9 setvar 𝑤 | |
7 | 6 | cv 1315 | . . . . . . . 8 class 𝑤 |
8 | 2 | cv 1315 | . . . . . . . . . 10 class 𝑥 |
9 | 3 | cv 1315 | . . . . . . . . . 10 class 𝑦 |
10 | 8, 9 | cop 3500 | . . . . . . . . 9 class 〈𝑥, 𝑦〉 |
11 | 4 | cv 1315 | . . . . . . . . 9 class 𝑧 |
12 | 10, 11 | cop 3500 | . . . . . . . 8 class 〈〈𝑥, 𝑦〉, 𝑧〉 |
13 | 7, 12 | wceq 1316 | . . . . . . 7 wff 𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 |
14 | 13, 1 | wa 103 | . . . . . 6 wff (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
15 | 14, 4 | wex 1453 | . . . . 5 wff ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
16 | 15, 3 | wex 1453 | . . . 4 wff ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
17 | 16, 2 | wex 1453 | . . 3 wff ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) |
18 | 17, 6 | cab 2103 | . 2 class {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
19 | 5, 18 | wceq 1316 | 1 wff {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
Colors of variables: wff set class |
This definition is referenced by: oprabid 5771 dfoprab2 5786 nfoprab1 5788 nfoprab2 5789 nfoprab3 5790 nfoprab 5791 oprabbid 5792 ssoprab2 5795 mpo0 5809 cbvoprab2 5812 eloprabga 5826 oprabrexex2 5996 eloprabi 6062 cnvoprab 6099 dftpos3 6127 |
Copyright terms: Public domain | W3C validator |