| 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 4006 | . . 3 ⊢ ran 𝐹 ⊆ ran 𝐹 | |
| 2 | 1 | biantru 529 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) |
| 3 | df-f 6565 | . 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹)) | |
| 4 | 2, 3 | bitr4i 278 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ⊆ wss 3951 ran crn 5686 Fn wfn 6556 ⟶wf 6557 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ss 3968 df-f 6565 |
| This theorem is referenced by: ffrn 6749 ffrnb 6750 fsn2 7156 coof 7721 offsplitfpar 8144 fo2ndf 8146 suppcoss 8232 fndmfisuppfi 9417 fndmfifsupp 9418 fin23lem17 10378 fin23lem32 10384 fnct 10577 yoniso 18330 psdmplcl 22166 1stckgen 23562 ovolicc2 25557 i1fadd 25730 i1fmul 25731 itg1addlem4 25734 i1fmulc 25738 clwlkclwwlklem2 30019 foresf1o 32523 fcoinver 32617 ofpreima2 32676 fmptunsnop 32709 suppssnn0 32809 locfinreflem 33839 pl1cn 33954 fvineqsneu 37412 poimirlem29 37656 poimirlem30 37657 itg2addnclem2 37679 mapdcl 41655 aks6d1c6isolem2 42176 tfsconcatrev 43361 wessf1ornlem 45190 unirnmap 45213 fsneqrn 45216 icccncfext 45902 stoweidlem29 46044 stoweidlem31 46046 stoweidlem59 46074 subsaliuncllem 46372 meadjiunlem 46480 uniimaprimaeqfv 47369 uniimaelsetpreimafv 47383 |
| Copyright terms: Public domain | W3C validator |