![]() |
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 3880 | . . 3 ⊢ ran 𝐹 ⊆ ran 𝐹 | |
2 | 1 | biantru 522 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) |
3 | df-f 6192 | . 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) | |
4 | 2, 3 | bitr4i 270 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 ⊆ wss 3830 ran crn 5408 Fn wfn 6183 ⟶wf 6184 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2751 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2760 df-cleq 2772 df-clel 2847 df-in 3837 df-ss 3844 df-f 6192 |
This theorem is referenced by: ffrn 6356 fsn2 6721 fo2ndf 7622 fndmfisuppfi 8640 fndmfifsupp 8641 fin23lem17 9558 fin23lem32 9564 fnct 9757 yoniso 17393 1stckgen 21866 ovolicc2 23826 i1fadd 23999 i1fmul 24000 itg1addlem4 24003 i1fmulc 24007 clwlkclwwlklem2 27506 foresf1o 30044 fcoinver 30121 ofpreima2 30173 locfinreflem 30745 pl1cn 30839 fvineqsneu 34130 poimirlem29 34359 poimirlem30 34360 itg2addnclem2 34382 mapdcl 38231 wessf1ornlem 40867 unirnmap 40894 fsneqrn 40897 icccncfext 41598 stoweidlem29 41743 stoweidlem31 41745 stoweidlem59 41773 subsaliuncllem 42069 meadjiunlem 42176 |
Copyright terms: Public domain | W3C validator |