Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-opab | GIF version |
Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.) |
Ref | Expression |
---|---|
df-opab | ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | 1, 2, 3 | copab 4025 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
5 | vz | . . . . . . . 8 setvar 𝑧 | |
6 | 5 | cv 1334 | . . . . . . 7 class 𝑧 |
7 | 2 | cv 1334 | . . . . . . . 8 class 𝑥 |
8 | 3 | cv 1334 | . . . . . . . 8 class 𝑦 |
9 | 7, 8 | cop 3563 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
10 | 6, 9 | wceq 1335 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
11 | 10, 1 | wa 103 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
12 | 11, 3 | wex 1472 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
13 | 12, 2 | wex 1472 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
14 | 13, 5 | cab 2143 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 4, 14 | wceq 1335 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Colors of variables: wff set class |
This definition is referenced by: opabss 4029 opabbid 4030 nfopab 4033 nfopab1 4034 nfopab2 4035 cbvopab 4036 cbvopab1 4038 cbvopab2 4039 cbvopab1s 4040 cbvopab2v 4042 unopab 4044 opabid 4218 elopab 4219 ssopab2 4236 iunopab 4242 elxpi 4603 rabxp 4624 csbxpg 4668 relopabi 4713 opabbrex 5866 dfoprab2 5869 dmoprab 5903 dfopab2 6138 cnvoprab 6182 |
Copyright terms: Public domain | W3C validator |