![]() |
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 5055 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3, 1 | wfn 5054 |
. . 3
![]() ![]() ![]() ![]() |
6 | 3 | crn 4478 |
. . . 4
![]() ![]() ![]() |
7 | 6, 2 | wss 3021 |
. . 3
![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | wa 103 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: feq1 5191 feq2 5192 feq3 5193 nff 5205 sbcfg 5207 ffn 5208 dffn2 5210 frn 5217 dffn3 5219 fss 5220 fco 5224 funssxp 5228 fun 5231 fnfco 5233 fssres 5234 fcoi2 5240 fintm 5244 fin 5245 f0 5249 fconst 5254 f1ssr 5271 fof 5281 dff1o2 5306 fun11iun 5322 ffoss 5333 dff2 5496 fmpt 5502 ffnfv 5510 ffvresb 5515 fpr 5534 fprg 5535 idref 5590 dff1o6 5609 fliftf 5632 1stcof 5992 2ndcof 5993 smores 6119 smores2 6121 iordsmo 6124 tfrcllembfn 6184 sbthlemi9 6781 inresflem 6860 frec2uzf1od 10020 frecuzrdgtcl 10026 fclim 10902 ennnfonelemf1 11723 cnrest2 12186 lmss 12196 psmetxrge0 12260 dvfgg 12530 nninfall 12788 |
Copyright terms: Public domain | W3C validator |