![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1of1 | Unicode version |
Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.) |
Ref | Expression |
---|---|
f1of1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f1o 5219 |
. 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 |
This theorem depends on definitions: df-bi 117 df-f1o 5219 |
This theorem is referenced by: f1of 5457 f1sng 5499 f1oresrab 5677 f1ocnvfvrneq 5777 isores3 5810 isoini2 5814 f1oiso 5821 f1opw2 6071 tposf12 6264 enssdom 6756 mapen 6840 ssenen 6845 phplem4 6849 phplem4on 6861 fidceq 6863 en2eqpr 6901 fiintim 6922 f1finf1o 6940 preimaf1ofi 6944 isotilem 6999 inresflem 7053 casefun 7078 endjusym 7089 dju1p1e2 7190 frec2uzled 10412 iseqf1olemnab 10471 iseqf1olemab 10472 iseqf1olemnanb 10473 hashen 10745 hashfacen 10797 negfi 11217 fisumss 11381 fprodssdc 11579 phimullem 12205 eulerthlemh 12211 ctinfom 12409 ssnnctlemct 12427 hmeoopn 13471 hmeocld 13472 hmeontr 13473 hmeoimaf1o 13474 iswomninnlem 14446 |
Copyright terms: Public domain | W3C validator |