Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > f1of | GIF version |
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.) |
Ref | Expression |
---|---|
f1of | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1of1 5125 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵) | |
2 | f1f 5092 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⟶wf 4898 –1-1→wf1 4899 –1-1-onto→wf1o 4901 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 df-f1 4907 df-f1o 4909 |
This theorem is referenced by: f1ofn 5127 f1oabexg 5138 f1ompt 5320 f1oresrab 5329 fsn 5335 fsnunf 5362 f1ocnvfv1 5417 f1ocnvfv2 5418 f1ocnvdm 5421 fcof1o 5429 isocnv 5451 isores2 5453 isotr 5456 isopolem 5461 isosolem 5463 f1oiso2 5466 f1ofveu 5500 smoiso 5917 f1oen2g 6235 en1 6279 enm 6294 fidceq 6330 dif1en 6337 fin0 6342 fin0or 6343 ac6sfi 6352 ordiso2 6357 cnrecnv 9510 |
Copyright terms: Public domain | W3C validator |