![]() |
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
![]() ![]() |
Ref | Expression |
---|---|
df-opab |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | copab 4075 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | vz |
. . . . . . . 8
![]() ![]() | |
6 | 5 | cv 1362 |
. . . . . . 7
![]() ![]() |
7 | 2 | cv 1362 |
. . . . . . . 8
![]() ![]() |
8 | 3 | cv 1362 |
. . . . . . . 8
![]() ![]() |
9 | 7, 8 | cop 3607 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | wceq 1363 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10, 1 | wa 104 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11, 3 | wex 1502 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 12, 2 | wex 1502 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13, 5 | cab 2173 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 4, 14 | wceq 1363 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: opabss 4079 opabbid 4080 nfopab 4083 nfopab1 4084 nfopab2 4085 cbvopab 4086 cbvopab1 4088 cbvopab2 4089 cbvopab1s 4090 cbvopab2v 4092 unopab 4094 opabid 4269 elopab 4270 ssopab2 4287 iunopab 4293 elxpi 4654 rabxp 4675 csbxpg 4719 relopabi 4764 opabbrex 5932 dfoprab2 5935 dmoprab 5969 dfopab2 6204 cnvoprab 6249 |
Copyright terms: Public domain | W3C validator |