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 5129 | . 2 | |
2 | 1 | simprbi 273 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 crn 4540 wfn 5118 wfo 5121 |
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 5129 |
This theorem is referenced by: dffo2 5349 foima 5350 fodmrnu 5353 f1imacnv 5384 foimacnv 5385 foun 5386 resdif 5389 fococnv2 5393 cbvfo 5686 cbvexfo 5687 isoini 5719 isoselem 5721 f1opw2 5976 fornex 6013 bren 6641 en1 6693 fopwdom 6730 mapen 6740 ssenen 6745 phplem4 6749 phplem4on 6761 ordiso2 6920 djuunr 6951 focdmex 10533 hashfacen 10579 ennnfonelemrn 11932 hmeontr 12482 |
Copyright terms: Public domain | W3C validator |