![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1f | GIF version |
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.) |
Ref | Expression |
---|---|
f1f | ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f1 5221 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
2 | 1 | simplbi 274 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ◡ccnv 4625 Fun wfun 5210 ⟶wf 5212 –1-1→wf1 5213 |
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-f1 5221 |
This theorem is referenced by: f1rn 5422 f1fn 5423 f1ss 5427 f1ssres 5430 f1of 5461 dff1o5 5470 fsnd 5504 cocan1 5787 f1o2ndf1 6228 brdomg 6747 f1dom2g 6755 f1domg 6757 dom3d 6773 f1imaen2g 6792 2dom 6804 xpdom2 6830 dom0 6837 phplem4dom 6861 isinfinf 6896 infm 6903 updjudhcoinlf 7078 updjudhcoinrg 7079 casef1 7088 djudom 7091 difinfsnlem 7097 difinfsn 7098 fihashf1rn 10763 ennnfonelemrn 12414 reeff1o 14125 pwle2 14668 |
Copyright terms: Public domain | W3C validator |