![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > forn | GIF version |
Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
forn | ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fo 5221 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
2 | 1 | simprbi 275 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ran crn 4626 Fn wfn 5210 –onto→wfo 5213 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-fo 5221 |
This theorem is referenced by: dffo2 5441 foima 5442 fodmrnu 5445 f1imacnv 5477 foimacnv 5478 foun 5479 resdif 5482 fococnv2 5486 foelcdmi 5567 cbvfo 5783 cbvexfo 5784 isoini 5816 isoselem 5818 canth 5826 f1opw2 6074 focdmex 6113 bren 6744 en1 6796 fopwdom 6833 mapen 6843 ssenen 6848 phplem4 6852 phplem4on 6864 ordiso2 7031 djuunr 7062 hashfacen 10809 ennnfonelemrn 12412 hmeontr 13684 |
Copyright terms: Public domain | W3C validator |