New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-mpt2 | 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 5652 for two arguments. (Contributed by SF, 5-Jan-2015.) |
Ref | Expression |
---|---|
df-mpt2 |
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 | cmpt2 5653 | . 2 |
7 | 1 | cv 1641 | . . . . . 6 |
8 | 7, 3 | wcel 1710 | . . . . 5 |
9 | 2 | cv 1641 | . . . . . 6 |
10 | 9, 4 | wcel 1710 | . . . . 5 |
11 | 8, 10 | wa 358 | . . . 4 |
12 | vz | . . . . . 6 | |
13 | 12 | cv 1641 | . . . . 5 |
14 | 13, 5 | wceq 1642 | . . . 4 |
15 | 11, 14 | wa 358 | . . 3 |
16 | 15, 1, 2, 12 | coprab 5527 | . 2 |
17 | 6, 16 | wceq 1642 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: mpt2eq123 5661 mpt2eq123dv 5663 mpt2eq3dva 5669 nfmpt21 5673 nfmpt22 5674 nfmpt2 5675 cbvmpt2x 5678 resmpt2 5697 fnov2 5707 mpt2mptx 5708 ovmpt4g 5710 ovmpt2x 5712 ovmpt2ga 5713 rnmpt2 5717 mpt2v 5719 fmpt2x 5730 releqmpt2 5809 composefn 5818 fnce 6176 |
Copyright terms: Public domain | W3C validator |