![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > forn | Unicode version |
Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
forn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fo 5137 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simprbi 273 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 5137 |
This theorem is referenced by: dffo2 5357 foima 5358 fodmrnu 5361 f1imacnv 5392 foimacnv 5393 foun 5394 resdif 5397 fococnv2 5401 cbvfo 5694 cbvexfo 5695 isoini 5727 isoselem 5729 f1opw2 5984 fornex 6021 bren 6649 en1 6701 fopwdom 6738 mapen 6748 ssenen 6753 phplem4 6757 phplem4on 6769 ordiso2 6928 djuunr 6959 focdmex 10565 hashfacen 10611 ennnfonelemrn 11968 hmeontr 12521 |
Copyright terms: Public domain | W3C validator |