Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-opab | Unicode 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 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | 1, 2, 3 | copab 4047 | . 2 |
5 | vz | . . . . . . . 8 | |
6 | 5 | cv 1347 | . . . . . . 7 |
7 | 2 | cv 1347 | . . . . . . . 8 |
8 | 3 | cv 1347 | . . . . . . . 8 |
9 | 7, 8 | cop 3584 | . . . . . . 7 |
10 | 6, 9 | wceq 1348 | . . . . . 6 |
11 | 10, 1 | wa 103 | . . . . 5 |
12 | 11, 3 | wex 1485 | . . . 4 |
13 | 12, 2 | wex 1485 | . . 3 |
14 | 13, 5 | cab 2156 | . 2 |
15 | 4, 14 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: opabss 4051 opabbid 4052 nfopab 4055 nfopab1 4056 nfopab2 4057 cbvopab 4058 cbvopab1 4060 cbvopab2 4061 cbvopab1s 4062 cbvopab2v 4064 unopab 4066 opabid 4240 elopab 4241 ssopab2 4258 iunopab 4264 elxpi 4625 rabxp 4646 csbxpg 4690 relopabi 4735 opabbrex 5894 dfoprab2 5897 dmoprab 5931 dfopab2 6165 cnvoprab 6210 |
Copyright terms: Public domain | W3C validator |