![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-f | GIF 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 | ⊢ (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ran 𝐹 ⊆ B)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | wf 4841 | . 2 wff 𝐹:A⟶B |
5 | 3, 1 | wfn 4840 | . . 3 wff 𝐹 Fn A |
6 | 3 | crn 4289 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wss 2911 | . . 3 wff ran 𝐹 ⊆ B |
8 | 5, 7 | wa 97 | . 2 wff (𝐹 Fn A ∧ ran 𝐹 ⊆ B) |
9 | 4, 8 | wb 98 | 1 wff (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ran 𝐹 ⊆ B)) |
Colors of variables: wff set class |
This definition is referenced by: feq1 4973 feq2 4974 feq3 4975 nff 4986 sbcfg 4988 ffn 4989 dffn2 4990 frn 4995 dffn3 4996 fss 4997 fco 4999 funssxp 5003 fun 5006 fnfco 5008 fssres 5009 fcoi2 5014 fintm 5018 fin 5019 f0 5023 fconst 5025 f1ssr 5041 fof 5049 dff1o2 5074 fun11iun 5090 ffoss 5101 dff2 5254 fmpt 5262 ffnfv 5266 ffvresb 5271 fpr 5288 fprg 5289 idref 5339 dff1o6 5359 fliftf 5382 1stcof 5732 2ndcof 5733 smores 5848 smores2 5850 iordsmo 5853 frec2uzf1od 8873 |
Copyright terms: Public domain | W3C validator |