![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-oprab | Structured version Visualization version Unicode version |
Description: Define the class
abstraction (class builder) of a collection of nested
ordered pairs (for use in defining operations). This is a special case
of Definition 4.16 of [TakeutiZaring] p. 14. Normally ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-oprab |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | vz |
. . 3
![]() ![]() | |
5 | 1, 2, 3, 4 | coprab 6316 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | vw |
. . . . . . . . 9
![]() ![]() | |
7 | 6 | cv 1454 |
. . . . . . . 8
![]() ![]() |
8 | 2 | cv 1454 |
. . . . . . . . . 10
![]() ![]() |
9 | 3 | cv 1454 |
. . . . . . . . . 10
![]() ![]() |
10 | 8, 9 | cop 3986 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
11 | 4 | cv 1454 |
. . . . . . . . 9
![]() ![]() |
12 | 10, 11 | cop 3986 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 7, 12 | wceq 1455 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13, 1 | wa 375 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 14, 4 | wex 1674 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 3 | wex 1674 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 2 | wex 1674 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 6 | cab 2448 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 5, 18 | wceq 1455 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: oprabid 6342 dfoprab2 6364 nfoprab1 6367 nfoprab2 6368 nfoprab3 6369 nfoprab 6370 oprabbid 6371 ssoprab2 6374 mpt20 6388 cbvoprab2 6391 eloprabga 6410 oprabrexex2 6810 eloprabi 6882 dftpos3 7017 meet0 16432 join0 16433 cnvoprab 28357 mppspstlem 30258 mppsval 30259 colinearex 30876 csboprabg 31776 |
Copyright terms: Public domain | W3C validator |