![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dffn3 | Structured version Visualization version GIF version |
Description: A function maps to its range. (Contributed by NM, 1-Sep-1999.) |
Ref | Expression |
---|---|
dffn3 | ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3657 | . . 3 ⊢ ran 𝐹 ⊆ ran 𝐹 | |
2 | 1 | biantru 525 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) |
3 | df-f 5930 | . 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) | |
4 | 2, 3 | bitr4i 267 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ⊆ wss 3607 ran crn 5144 Fn wfn 5921 ⟶wf 5922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-in 3614 df-ss 3621 df-f 5930 |
This theorem is referenced by: ffrn 6093 fsn2 6443 fo2ndf 7329 fndmfisuppfi 8328 fndmfifsupp 8329 fin23lem17 9198 fin23lem32 9204 fnct 9397 yoniso 16972 1stckgen 21405 ovolicc2 23336 itg1val2 23496 i1fadd 23507 i1fmul 23508 itg1addlem4 23511 i1fmulc 23515 clwlkclwwlklem2 26966 foresf1o 29469 fcoinver 29544 ofpreima2 29594 locfinreflem 30035 pl1cn 30129 poimirlem29 33568 poimirlem30 33569 itg2addnclem2 33592 mapdcl 37259 wessf1ornlem 39685 unirnmap 39714 fsneqrn 39717 icccncfext 40418 stoweidlem29 40564 stoweidlem31 40566 stoweidlem59 40594 subsaliuncllem 40893 meadjiunlem 41000 |
Copyright terms: Public domain | W3C validator |