![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-opab | Structured version Visualization version 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 4476 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | vz |
. . . . . . . 8
![]() ![]() | |
6 | 5 | cv 1454 |
. . . . . . 7
![]() ![]() |
7 | 2 | cv 1454 |
. . . . . . . 8
![]() ![]() |
8 | 3 | cv 1454 |
. . . . . . . 8
![]() ![]() |
9 | 7, 8 | cop 3986 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | wceq 1455 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10, 1 | wa 375 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11, 3 | wex 1674 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 12, 2 | wex 1674 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13, 5 | cab 2448 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 4, 14 | wceq 1455 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: opabss 4480 opabbid 4481 nfopab 4484 nfopab1 4485 nfopab2 4486 cbvopab 4487 cbvopab1 4489 cbvopab2 4490 cbvopab1s 4491 cbvopab2v 4493 unopab 4494 opabid 4725 elopab 4726 ssopab2 4744 iunopab 4754 dfid3 4772 elxpi 4872 rabxp 4893 csbxp 4938 relopabi 4981 opabbrexOLD 6363 dfoprab2 6369 dmoprab 6409 opabex2 6763 dfopab2 6879 brdom7disj 8990 brdom6disj 8991 cnvoprab 28360 areacirc 32083 dropab1 36845 dropab2 36846 csbxpgOLD 37255 csbxpgVD 37332 relopabVD 37339 |
Copyright terms: Public domain | W3C validator |