![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1ofo | Unicode version |
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.) |
Ref | Expression |
---|---|
f1ofo |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dff1o3 5467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 274 |
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 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 df-f 5220 df-f1 5221 df-fo 5222 df-f1o 5223 |
This theorem is referenced by: f1imacnv 5478 f1ococnv2 5488 fo00 5497 isoini 5818 isoselem 5820 f1opw2 6076 f1dmex 6116 bren 6746 f1oeng 6756 en1 6798 mapen 6845 ssenen 6850 phplem4 6854 phplem4on 6866 dif1en 6878 fiintim 6927 fidcenumlemim 6950 supisolem 7006 ordiso2 7033 djuunr 7064 omct 7115 ctssexmid 7147 1fv 10138 hashfacen 10815 fsumf1o 11397 fisumss 11399 fprodf1o 11595 fprodssdc 11597 ennnfonelemrn 12419 ennnfonelemnn0 12422 ennnfonelemim 12424 exmidunben 12426 ctinfomlemom 12427 ctinfom 12428 qnnen 12431 enctlem 12432 ssomct 12445 xpsfrn 12768 hmeontr 13749 hmeoimaf1o 13750 subctctexmid 14686 exmidsbthrlem 14706 sbthomlem 14709 |
Copyright terms: Public domain | W3C validator |