![]() |
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 5086 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
2 | 1 | simplbi 270 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ◡ccnv 4498 Fun wfun 5075 ⟶wf 5077 –1-1→wf1 5078 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-f1 5086 |
This theorem is referenced by: f1rn 5287 f1fn 5288 f1ss 5292 f1ssres 5295 f1of 5323 dff1o5 5332 cocan1 5642 f1o2ndf1 6079 brdomg 6596 f1dom2g 6604 f1domg 6606 dom3d 6622 f1imaen2g 6641 2dom 6653 xpdom2 6678 dom0 6685 phplem4dom 6709 isinfinf 6744 infm 6751 updjudhcoinlf 6917 updjudhcoinrg 6918 casef1 6927 djudom 6930 difinfsnlem 6936 difinfsn 6937 fihashf1rn 10428 ennnfonelemrn 11777 pwle2 12885 |
Copyright terms: Public domain | W3C validator |