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 3958 | . 2 |
5 | vz | . . . . . . . 8 | |
6 | 5 | cv 1315 | . . . . . . 7 |
7 | 2 | cv 1315 | . . . . . . . 8 |
8 | 3 | cv 1315 | . . . . . . . 8 |
9 | 7, 8 | cop 3500 | . . . . . . 7 |
10 | 6, 9 | wceq 1316 | . . . . . 6 |
11 | 10, 1 | wa 103 | . . . . 5 |
12 | 11, 3 | wex 1453 | . . . 4 |
13 | 12, 2 | wex 1453 | . . 3 |
14 | 13, 5 | cab 2103 | . 2 |
15 | 4, 14 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: opabss 3962 opabbid 3963 nfopab 3966 nfopab1 3967 nfopab2 3968 cbvopab 3969 cbvopab1 3971 cbvopab2 3972 cbvopab1s 3973 cbvopab2v 3975 unopab 3977 opabid 4149 elopab 4150 ssopab2 4167 iunopab 4173 elxpi 4525 rabxp 4546 csbxpg 4590 relopabi 4635 opabbrex 5783 dfoprab2 5786 dmoprab 5820 dfopab2 6055 cnvoprab 6099 |
Copyright terms: Public domain | W3C validator |