![]() |
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 x and y 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 | ⊢ {〈x, y〉 ∣ φ} = {z ∣ ∃x∃y(z = 〈x, y〉 ∧ φ)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff φ | |
2 | vx | . . 3 setvar x | |
3 | vy | . . 3 setvar y | |
4 | 1, 2, 3 | copab 3808 | . 2 class {〈x, y〉 ∣ φ} |
5 | vz | . . . . . . . 8 setvar z | |
6 | 5 | cv 1241 | . . . . . . 7 class z |
7 | 2 | cv 1241 | . . . . . . . 8 class x |
8 | 3 | cv 1241 | . . . . . . . 8 class y |
9 | 7, 8 | cop 3370 | . . . . . . 7 class 〈x, y〉 |
10 | 6, 9 | wceq 1242 | . . . . . 6 wff z = 〈x, y〉 |
11 | 10, 1 | wa 97 | . . . . 5 wff (z = 〈x, y〉 ∧ φ) |
12 | 11, 3 | wex 1378 | . . . 4 wff ∃y(z = 〈x, y〉 ∧ φ) |
13 | 12, 2 | wex 1378 | . . 3 wff ∃x∃y(z = 〈x, y〉 ∧ φ) |
14 | 13, 5 | cab 2023 | . 2 class {z ∣ ∃x∃y(z = 〈x, y〉 ∧ φ)} |
15 | 4, 14 | wceq 1242 | 1 wff {〈x, y〉 ∣ φ} = {z ∣ ∃x∃y(z = 〈x, y〉 ∧ φ)} |
Colors of variables: wff set class |
This definition is referenced by: opabss 3812 opabbid 3813 nfopab 3816 nfopab1 3817 nfopab2 3818 cbvopab 3819 cbvopab1 3821 cbvopab2 3822 cbvopab1s 3823 cbvopab2v 3825 unopab 3827 opabid 3985 elopab 3986 ssopab2 4003 iunopab 4009 elxpi 4304 rabxp 4323 csbxpg 4364 relopabi 4406 opabbrex 5491 dfoprab2 5494 dmoprab 5527 dfopab2 5757 |
Copyright terms: Public domain | W3C validator |