![]() |
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 3859 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | vz |
. . . . . . . 8
![]() ![]() | |
6 | 5 | cv 1284 |
. . . . . . 7
![]() ![]() |
7 | 2 | cv 1284 |
. . . . . . . 8
![]() ![]() |
8 | 3 | cv 1284 |
. . . . . . . 8
![]() ![]() |
9 | 7, 8 | cop 3420 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | wceq 1285 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10, 1 | wa 102 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11, 3 | wex 1422 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 12, 2 | wex 1422 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13, 5 | cab 2069 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 4, 14 | wceq 1285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: opabss 3863 opabbid 3864 nfopab 3867 nfopab1 3868 nfopab2 3869 cbvopab 3870 cbvopab1 3872 cbvopab2 3873 cbvopab1s 3874 cbvopab2v 3876 unopab 3878 opabid 4041 elopab 4042 ssopab2 4059 iunopab 4065 elxpi 4408 rabxp 4427 csbxpg 4468 relopabi 4512 opabbrex 5602 dfoprab2 5605 dmoprab 5638 dfopab2 5868 cnvoprab 5908 |
Copyright terms: Public domain | W3C validator |