![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1of1 | GIF version |
Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.) |
Ref | Expression |
---|---|
f1of1 | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f1o 5223 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) | |
2 | 1 | simplbi 274 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 –1-1→wf1 5213 –onto→wfo 5214 –1-1-onto→wf1o 5215 |
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 5223 |
This theorem is referenced by: f1of 5461 f1sng 5503 f1oresrab 5681 f1ocnvfvrneq 5782 isores3 5815 isoini2 5819 f1oiso 5826 f1opw2 6076 tposf12 6269 enssdom 6761 mapen 6845 ssenen 6850 phplem4 6854 phplem4on 6866 fidceq 6868 en2eqpr 6906 fiintim 6927 f1finf1o 6945 preimaf1ofi 6949 isotilem 7004 inresflem 7058 casefun 7083 endjusym 7094 dju1p1e2 7195 frec2uzled 10428 iseqf1olemnab 10487 iseqf1olemab 10488 iseqf1olemnanb 10489 hashen 10763 hashfacen 10815 negfi 11235 fisumss 11399 fprodssdc 11597 phimullem 12224 eulerthlemh 12230 ctinfom 12428 ssnnctlemct 12446 f1ocpbllem 12730 f1ovscpbl 12732 xpsff1o2 12769 eqgen 13084 hmeoopn 13747 hmeocld 13748 hmeontr 13749 hmeoimaf1o 13750 iswomninnlem 14733 |
Copyright terms: Public domain | W3C validator |