![]() |
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 5021 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simprbi 269 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 |
This theorem depends on definitions: df-bi 115 df-fo 5021 |
This theorem is referenced by: dffo2 5237 foima 5238 fodmrnu 5241 f1imacnv 5270 foimacnv 5271 foun 5272 resdif 5275 fococnv2 5279 cbvfo 5564 cbvexfo 5565 isoini 5597 isoselem 5599 f1opw2 5850 fornex 5886 bren 6464 en1 6516 fopwdom 6552 mapen 6562 ssenen 6567 phplem4 6571 phplem4on 6583 ordiso2 6728 djuunr 6758 focdmex 10195 hashfacen 10241 |
Copyright terms: Public domain | W3C validator |