![]() |
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 5241 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simprbi 275 |
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 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-fo 5241 |
This theorem is referenced by: dffo2 5461 foima 5462 fodmrnu 5465 f1imacnv 5497 foimacnv 5498 foun 5499 resdif 5502 fococnv2 5506 foelcdmi 5589 cbvfo 5807 cbvexfo 5808 isoini 5840 isoselem 5842 canth 5850 f1opw2 6100 focdmex 6140 bren 6773 en1 6825 fopwdom 6864 mapen 6874 ssenen 6879 phplem4 6883 phplem4on 6895 ordiso2 7064 djuunr 7095 hashfacen 10848 ennnfonelemrn 12470 imasival 12783 imasaddfnlemg 12791 xpsfrn 12826 imasgrp2 13052 imasrng 13310 imasring 13414 hmeontr 14273 |
Copyright terms: Public domain | W3C validator |