![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-mpo | Unicode version |
Description: Define maps-to notation
for defining an operation via a rule. Read as
"the operation defined by the map from ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-mpo |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx |
. . 3
![]() ![]() | |
2 | vy |
. . 3
![]() ![]() | |
3 | cA |
. . 3
![]() ![]() | |
4 | cB |
. . 3
![]() ![]() | |
5 | cC |
. . 3
![]() ![]() | |
6 | 1, 2, 3, 4, 5 | cmpo 5871 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1 | cv 1352 |
. . . . . 6
![]() ![]() |
8 | 7, 3 | wcel 2148 |
. . . . 5
![]() ![]() ![]() ![]() |
9 | 2 | cv 1352 |
. . . . . 6
![]() ![]() |
10 | 9, 4 | wcel 2148 |
. . . . 5
![]() ![]() ![]() ![]() |
11 | 8, 10 | wa 104 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | vz |
. . . . . 6
![]() ![]() | |
13 | 12 | cv 1352 |
. . . . 5
![]() ![]() |
14 | 13, 5 | wceq 1353 |
. . . 4
![]() ![]() ![]() ![]() |
15 | 11, 14 | wa 104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 1, 2, 12 | coprab 5870 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 6, 16 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: mpoeq123 5928 mpoeq123dva 5930 mpoeq3dva 5933 nfmpo1 5936 nfmpo2 5937 nfmpo 5938 mpo0 5939 cbvmpox 5947 mpov 5959 mpomptx 5960 resmpo 5967 mpofun 5971 mpo2eqb 5978 rnmpo 5979 reldmmpo 5980 ovmpt4g 5991 elmpocl 6063 fmpox 6195 f1od2 6230 tposmpo 6276 erovlem 6621 xpcomco 6820 dfplpq2 7341 dfmpq2 7342 |
Copyright terms: Public domain | W3C validator |