![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-mpt | Unicode version |
Description: Define maps-to notation
for defining a function via a rule. Read as
"the function defined by the map from ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-mpt |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx |
. . 3
![]() ![]() | |
2 | cA |
. . 3
![]() ![]() | |
3 | cB |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | cmpt 3809 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1 | cv 1241 |
. . . . 5
![]() ![]() |
6 | 5, 2 | wcel 1390 |
. . . 4
![]() ![]() ![]() ![]() |
7 | vy |
. . . . . 6
![]() ![]() | |
8 | 7 | cv 1241 |
. . . . 5
![]() ![]() |
9 | 8, 3 | wceq 1242 |
. . . 4
![]() ![]() ![]() ![]() |
10 | 6, 9 | wa 97 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10, 1, 7 | copab 3808 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 4, 11 | wceq 1242 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: mpteq12f 3828 nfmpt 3840 nfmpt1 3841 cbvmpt 3842 mptv 3844 fconstmpt 4330 rnmpt 4525 resmpt 4599 mptresid 4603 mptpreima 4757 funmpt 4881 dfmpt3 4964 mptfng 4967 mptun 4972 dffn5im 5162 fvmptss2 5190 fvmptg 5191 fndmin 5217 f1ompt 5263 fmptco 5273 mpt2mptx 5537 f1ocnvd 5644 dftpos4 5819 |
Copyright terms: Public domain | W3C validator |