![]() |
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 3928 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | vz |
. . . . . . . 8
![]() ![]() | |
6 | 5 | cv 1298 |
. . . . . . 7
![]() ![]() |
7 | 2 | cv 1298 |
. . . . . . . 8
![]() ![]() |
8 | 3 | cv 1298 |
. . . . . . . 8
![]() ![]() |
9 | 7, 8 | cop 3477 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | wceq 1299 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10, 1 | wa 103 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11, 3 | wex 1436 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 12, 2 | wex 1436 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13, 5 | cab 2086 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 4, 14 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: opabss 3932 opabbid 3933 nfopab 3936 nfopab1 3937 nfopab2 3938 cbvopab 3939 cbvopab1 3941 cbvopab2 3942 cbvopab1s 3943 cbvopab2v 3945 unopab 3947 opabid 4117 elopab 4118 ssopab2 4135 iunopab 4141 elxpi 4493 rabxp 4514 csbxpg 4558 relopabi 4603 opabbrex 5747 dfoprab2 5750 dmoprab 5784 dfopab2 6017 cnvoprab 6061 |
Copyright terms: Public domain | W3C validator |