![]() |
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 3999 | . . 3 ⊢ ran 𝐹 ⊆ ran 𝐹 | |
2 | 1 | biantru 528 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) |
3 | df-f 6553 | . 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) | |
4 | 2, 3 | bitr4i 277 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ⊆ wss 3944 ran crn 5679 Fn wfn 6544 ⟶wf 6545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ss 3961 df-f 6553 |
This theorem is referenced by: ffrn 6736 ffrnb 6737 fsn2 7145 coof 7708 offsplitfpar 8124 fo2ndf 8126 suppcoss 8213 fndmfisuppfi 9402 fndmfifsupp 9403 fin23lem17 10363 fin23lem32 10369 fnct 10562 yoniso 18280 psdmplcl 22109 1stckgen 23502 ovolicc2 25495 i1fadd 25668 i1fmul 25669 itg1addlem4 25672 itg1addlem4OLD 25673 i1fmulc 25677 clwlkclwwlklem2 29882 foresf1o 32378 fcoinver 32473 ofpreima2 32533 suppssnn0 32657 locfinreflem 33572 pl1cn 33687 fvineqsneu 37021 poimirlem29 37253 poimirlem30 37254 itg2addnclem2 37276 mapdcl 41256 aks6d1c6isolem2 41778 tfsconcatrev 42919 wessf1ornlem 44697 unirnmap 44720 fsneqrn 44723 icccncfext 45413 stoweidlem29 45555 stoweidlem31 45557 stoweidlem59 45585 subsaliuncllem 45883 meadjiunlem 45991 uniimaprimaeqfv 46859 uniimaelsetpreimafv 46873 |
Copyright terms: Public domain | W3C validator |