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 3988 | . 2 |
5 | vz | . . . . . . . 8 | |
6 | 5 | cv 1330 | . . . . . . 7 |
7 | 2 | cv 1330 | . . . . . . . 8 |
8 | 3 | cv 1330 | . . . . . . . 8 |
9 | 7, 8 | cop 3530 | . . . . . . 7 |
10 | 6, 9 | wceq 1331 | . . . . . 6 |
11 | 10, 1 | wa 103 | . . . . 5 |
12 | 11, 3 | wex 1468 | . . . 4 |
13 | 12, 2 | wex 1468 | . . 3 |
14 | 13, 5 | cab 2125 | . 2 |
15 | 4, 14 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: opabss 3992 opabbid 3993 nfopab 3996 nfopab1 3997 nfopab2 3998 cbvopab 3999 cbvopab1 4001 cbvopab2 4002 cbvopab1s 4003 cbvopab2v 4005 unopab 4007 opabid 4179 elopab 4180 ssopab2 4197 iunopab 4203 elxpi 4555 rabxp 4576 csbxpg 4620 relopabi 4665 opabbrex 5815 dfoprab2 5818 dmoprab 5852 dfopab2 6087 cnvoprab 6131 |
Copyright terms: Public domain | W3C validator |