![]() |
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 3996 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
5 | vz | . . . . . . . 8 setvar 𝑧 | |
6 | 5 | cv 1331 | . . . . . . 7 class 𝑧 |
7 | 2 | cv 1331 | . . . . . . . 8 class 𝑥 |
8 | 3 | cv 1331 | . . . . . . . 8 class 𝑦 |
9 | 7, 8 | cop 3535 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
10 | 6, 9 | wceq 1332 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
11 | 10, 1 | wa 103 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
12 | 11, 3 | wex 1469 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
13 | 12, 2 | wex 1469 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
14 | 13, 5 | cab 2126 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 4, 14 | wceq 1332 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Colors of variables: wff set class |
This definition is referenced by: opabss 4000 opabbid 4001 nfopab 4004 nfopab1 4005 nfopab2 4006 cbvopab 4007 cbvopab1 4009 cbvopab2 4010 cbvopab1s 4011 cbvopab2v 4013 unopab 4015 opabid 4187 elopab 4188 ssopab2 4205 iunopab 4211 elxpi 4563 rabxp 4584 csbxpg 4628 relopabi 4673 opabbrex 5823 dfoprab2 5826 dmoprab 5860 dfopab2 6095 cnvoprab 6139 |
Copyright terms: Public domain | W3C validator |