![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE 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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 5514 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1 | cv 1242 |
. . . . . 6
![]() ![]() |
8 | 7, 3 | wcel 1393 |
. . . . 5
![]() ![]() ![]() ![]() |
9 | 2 | cv 1242 |
. . . . . 6
![]() ![]() |
10 | 9, 4 | wcel 1393 |
. . . . 5
![]() ![]() ![]() ![]() |
11 | 8, 10 | wa 97 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | vz |
. . . . . 6
![]() ![]() | |
13 | 12 | cv 1242 |
. . . . 5
![]() ![]() |
14 | 13, 5 | wceq 1243 |
. . . 4
![]() ![]() ![]() ![]() |
15 | 11, 14 | wa 97 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 1, 2, 12 | coprab 5513 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 6, 16 | wceq 1243 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: mpt2eq123 5564 mpt2eq123dva 5566 mpt2eq3dva 5569 nfmpt21 5571 nfmpt22 5572 nfmpt2 5573 mpt20 5574 cbvmpt2x 5582 mpt2v 5594 mpt2mptx 5595 resmpt2 5599 mpt2fun 5603 mpt22eqb 5610 rnmpt2 5611 reldmmpt2 5612 ovmpt4g 5623 elmpt2cl 5698 fmpt2x 5826 tposmpt2 5896 erovlem 6198 xpcomco 6300 dfplpq2 6452 dfmpq2 6453 |
Copyright terms: Public domain | W3C validator |