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 5179 | . 2 wff 𝐹:𝐴⟶𝐵 |
5 | 3, 1 | wfn 5178 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 4600 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wss 3112 | . . 3 wff ran 𝐹 ⊆ 𝐵 |
8 | 5, 7 | wa 103 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) |
9 | 4, 8 | wb 104 | 1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: feq1 5315 feq2 5316 feq3 5317 nff 5329 sbcfg 5331 ffn 5332 dffn2 5334 frn 5341 dffn3 5343 fss 5344 fco 5348 funssxp 5352 fun 5355 fnfco 5357 fssres 5358 fcoi2 5364 fintm 5368 fin 5369 f0 5373 fconst 5378 f1ssr 5395 fof 5405 dff1o2 5432 fun11iun 5448 ffoss 5459 dff2 5624 fmpt 5630 ffnfv 5638 ffvresb 5643 fpr 5662 fprg 5663 idref 5720 dff1o6 5739 fliftf 5762 1stcof 6124 2ndcof 6125 smores 6252 smores2 6254 iordsmo 6257 tfrcllembfn 6317 sbthlemi9 6922 inresflem 7017 frec2uzf1od 10332 frecuzrdgtcl 10338 fclim 11225 ennnfonelemf1 12314 cnrest2 12803 lmss 12813 psmetxrge0 12899 dvfgg 13224 nninfall 13750 |
Copyright terms: Public domain | W3C validator |