![]() |
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 5565 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1 | cv 1284 |
. . . . . 6
![]() ![]() |
8 | 7, 3 | wcel 1434 |
. . . . 5
![]() ![]() ![]() ![]() |
9 | 2 | cv 1284 |
. . . . . 6
![]() ![]() |
10 | 9, 4 | wcel 1434 |
. . . . 5
![]() ![]() ![]() ![]() |
11 | 8, 10 | wa 102 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | vz |
. . . . . 6
![]() ![]() | |
13 | 12 | cv 1284 |
. . . . 5
![]() ![]() |
14 | 13, 5 | wceq 1285 |
. . . 4
![]() ![]() ![]() ![]() |
15 | 11, 14 | wa 102 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 1, 2, 12 | coprab 5564 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 6, 16 | wceq 1285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: mpt2eq123 5615 mpt2eq123dva 5617 mpt2eq3dva 5620 nfmpt21 5622 nfmpt22 5623 nfmpt2 5624 mpt20 5625 cbvmpt2x 5633 mpt2v 5645 mpt2mptx 5646 resmpt2 5650 mpt2fun 5654 mpt22eqb 5661 rnmpt2 5662 reldmmpt2 5663 ovmpt4g 5674 elmpt2cl 5749 fmpt2x 5877 f1od2 5907 tposmpt2 5950 erovlem 6285 xpcomco 6391 dfplpq2 6658 dfmpq2 6659 |
Copyright terms: Public domain | W3C validator |