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 4039 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 5838 | . 2 |
7 | 1 | cv 1341 | . . . . . 6 |
8 | 7, 3 | wcel 2135 | . . . . 5 |
9 | 2 | cv 1341 | . . . . . 6 |
10 | 9, 4 | wcel 2135 | . . . . 5 |
11 | 8, 10 | wa 103 | . . . 4 |
12 | vz | . . . . . 6 | |
13 | 12 | cv 1341 | . . . . 5 |
14 | 13, 5 | wceq 1342 | . . . 4 |
15 | 11, 14 | wa 103 | . . 3 |
16 | 15, 1, 2, 12 | coprab 5837 | . 2 |
17 | 6, 16 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: mpoeq123 5892 mpoeq123dva 5894 mpoeq3dva 5897 nfmpo1 5900 nfmpo2 5901 nfmpo 5902 mpo0 5903 cbvmpox 5911 mpov 5923 mpomptx 5924 resmpo 5931 mpofun 5935 mpo2eqb 5942 rnmpo 5943 reldmmpo 5944 ovmpt4g 5955 elmpocl 6030 fmpox 6160 f1od2 6194 tposmpo 6240 erovlem 6584 xpcomco 6783 dfplpq2 7286 dfmpq2 7287 |
Copyright terms: Public domain | W3C validator |