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 5099 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
2 | 1 | simprbi 273 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1316 ran crn 4510 Fn wfn 5088 –onto→wfo 5091 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-fo 5099 |
This theorem is referenced by: dffo2 5319 foima 5320 fodmrnu 5323 f1imacnv 5352 foimacnv 5353 foun 5354 resdif 5357 fococnv2 5361 cbvfo 5654 cbvexfo 5655 isoini 5687 isoselem 5689 f1opw2 5944 fornex 5981 bren 6609 en1 6661 fopwdom 6698 mapen 6708 ssenen 6713 phplem4 6717 phplem4on 6729 ordiso2 6888 djuunr 6919 focdmex 10501 hashfacen 10547 ennnfonelemrn 11859 hmeontr 12409 |
Copyright terms: Public domain | W3C validator |