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 (in ) to ". An extension of df-mpt 4052 for two arguments. (Contributed by NM, 17-Feb-2008.) |
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 5855 | . 2 |
7 | 1 | cv 1347 | . . . . . 6 |
8 | 7, 3 | wcel 2141 | . . . . 5 |
9 | 2 | cv 1347 | . . . . . 6 |
10 | 9, 4 | wcel 2141 | . . . . 5 |
11 | 8, 10 | wa 103 | . . . 4 |
12 | vz | . . . . . 6 | |
13 | 12 | cv 1347 | . . . . 5 |
14 | 13, 5 | wceq 1348 | . . . 4 |
15 | 11, 14 | wa 103 | . . 3 |
16 | 15, 1, 2, 12 | coprab 5854 | . 2 |
17 | 6, 16 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: mpoeq123 5912 mpoeq123dva 5914 mpoeq3dva 5917 nfmpo1 5920 nfmpo2 5921 nfmpo 5922 mpo0 5923 cbvmpox 5931 mpov 5943 mpomptx 5944 resmpo 5951 mpofun 5955 mpo2eqb 5962 rnmpo 5963 reldmmpo 5964 ovmpt4g 5975 elmpocl 6047 fmpox 6179 f1od2 6214 tposmpo 6260 erovlem 6605 xpcomco 6804 dfplpq2 7316 dfmpq2 7317 |
Copyright terms: Public domain | W3C validator |