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 4908 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
2 | 1 | simprbi 260 | 1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1243 ran crn 4346 Fn wfn 4897 –onto→wfo 4900 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 |
This theorem depends on definitions: df-bi 110 df-fo 4908 |
This theorem is referenced by: dffo2 5110 foima 5111 fodmrnu 5114 f1imacnv 5143 foimacnv 5144 foun 5145 resdif 5148 fococnv2 5152 cbvfo 5425 cbvexfo 5426 isoini 5457 isoselem 5459 f1opw2 5706 fornex 5742 bren 6228 en1 6279 fopwdom 6310 phplem4 6318 phplem4on 6329 ordiso2 6357 |
Copyright terms: Public domain | W3C validator |