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 3624 | . . 3 ⊢ ran 𝐹 ⊆ ran 𝐹 | |
2 | 1 | biantru 526 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) |
3 | df-f 5892 | . 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) | |
4 | 2, 3 | bitr4i 267 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 ⊆ wss 3574 ran crn 5115 Fn wfn 5883 ⟶wf 5884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-in 3581 df-ss 3588 df-f 5892 |
This theorem is referenced by: ffrn 6055 fsn2 6403 fo2ndf 7284 fndmfisuppfi 8287 fndmfifsupp 8288 fin23lem17 9160 fin23lem32 9166 fnct 9359 yoniso 16925 1stckgen 21357 ovolicc2 23290 itg1val2 23451 i1fadd 23462 i1fmul 23463 itg1addlem4 23466 i1fmulc 23470 clwlkclwwlklem2 26901 foresf1o 29343 fcoinver 29418 ofpreima2 29466 locfinreflem 29907 pl1cn 30001 poimirlem29 33438 poimirlem30 33439 itg2addnclem2 33462 mapdcl 36942 wessf1ornlem 39371 unirnmap 39400 fsneqrn 39403 icccncfext 40100 stoweidlem29 40246 stoweidlem31 40248 stoweidlem59 40276 subsaliuncllem 40575 meadjiunlem 40682 |
Copyright terms: Public domain | W3C validator |