![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ffund | Structured version Visualization version GIF version |
Description: A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Ref | Expression |
---|---|
ffund.1 | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
Ref | Expression |
---|---|
ffund | ⊢ (𝜑 → Fun 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffund.1 | . 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
2 | ffun 6086 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Fun wfun 5920 ⟶wf 5922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 df-fn 5929 df-f 5930 |
This theorem is referenced by: fofun 6154 fmptco 6436 evlslem3 19562 mdegldg 23871 uhgrfun 26006 vdegp1bi 26489 wlkreslem 26622 wlkres 26623 gneispacefun 38752 limsuppnfdlem 40251 climxrrelem 40299 climxrre 40300 liminfvalxr 40333 xlimxrre 40375 subsaliuncllem 40893 ovnovollem2 41192 preimaioomnf 41250 smfresal 41316 smfres 41318 smfco 41330 |
Copyright terms: Public domain | W3C validator |