![]() |
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 | ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | wf 5212 | . 2 wff 𝐹:𝐴⟶𝐵 |
5 | 3, 1 | wfn 5211 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 4627 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wss 3129 | . . 3 wff ran 𝐹 ⊆ 𝐵 |
8 | 5, 7 | wa 104 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) |
9 | 4, 8 | wb 105 | 1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: feq1 5348 feq2 5349 feq3 5350 nff 5362 sbcfg 5364 ffn 5365 dffn2 5367 frn 5374 dffn3 5376 fss 5377 fco 5381 funssxp 5385 fun 5388 fnfco 5390 fssres 5391 fcoi2 5397 fintm 5401 fin 5402 f0 5406 fconst 5411 f1ssr 5428 fof 5438 dff1o2 5466 fun11iun 5482 ffoss 5493 dff2 5660 fmpt 5666 ffnfv 5674 ffvresb 5679 fpr 5698 fprg 5699 idref 5757 dff1o6 5776 fliftf 5799 1stcof 6163 2ndcof 6164 smores 6292 smores2 6294 iordsmo 6297 tfrcllembfn 6357 sbthlemi9 6963 inresflem 7058 frec2uzf1od 10405 frecuzrdgtcl 10411 fclim 11301 ennnfonelemf1 12418 srgfcl 13154 cnrest2 13706 lmss 13716 psmetxrge0 13802 dvfgg 14127 nninfall 14728 |
Copyright terms: Public domain | W3C validator |