![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-f | Unicode version |
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cF |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | wf 5231 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3, 1 | wfn 5230 |
. . 3
![]() ![]() ![]() ![]() |
6 | 3 | crn 4645 |
. . . 4
![]() ![]() ![]() |
7 | 6, 2 | wss 3144 |
. . 3
![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: feq1 5367 feq2 5368 feq3 5369 nff 5381 sbcfg 5383 ffn 5384 dffn2 5386 frn 5393 dffn3 5395 fss 5396 fco 5400 funssxp 5404 fun 5407 fnfco 5409 fssres 5410 fcoi2 5416 fintm 5420 fin 5421 f0 5425 fconst 5430 f1ssr 5447 fof 5457 dff1o2 5485 fun11iun 5501 ffoss 5512 dff2 5681 fmpt 5687 ffnfv 5695 ffvresb 5700 fpr 5719 fprg 5720 idref 5778 dff1o6 5798 fliftf 5821 1stcof 6189 2ndcof 6190 smores 6318 smores2 6320 iordsmo 6323 tfrcllembfn 6383 sbthlemi9 6995 inresflem 7090 frec2uzf1od 10439 frecuzrdgtcl 10445 fclim 11337 ennnfonelemf1 12472 resmhm2b 12956 srgfcl 13344 cnrest2 14213 lmss 14223 psmetxrge0 14309 dvfgg 14634 nninfall 15237 |
Copyright terms: Public domain | W3C validator |