![]() |
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 4972 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
2 | 1 | simplbi 268 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ◡ccnv 4398 Fun wfun 4961 ⟶wf 4963 –1-1→wf1 4964 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 df-f1 4972 |
This theorem is referenced by: f1rn 5163 f1fn 5164 f1ss 5168 f1ssres 5171 f1of 5199 dff1o5 5208 cocan1 5504 f1o2ndf1 5926 brdomg 6393 f1dom2g 6401 f1domg 6403 dom3d 6419 f1imaen2g 6438 2dom 6450 xpdom2 6475 dom0 6482 phplem4dom 6506 isinfinf 6541 infm 6545 updjudhcoinlf 6676 updjudhcoinrg 6677 casef1 6686 djudom 6692 fihashf1rn 10030 |
Copyright terms: Public domain | W3C validator |