![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1f | Unicode version |
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.) |
Ref | Expression |
---|---|
f1f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f1 5015 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 268 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 5015 |
This theorem is referenced by: f1rn 5211 f1fn 5212 f1ss 5216 f1ssres 5219 f1of 5247 dff1o5 5256 cocan1 5558 f1o2ndf1 5985 brdomg 6455 f1dom2g 6463 f1domg 6465 dom3d 6481 f1imaen2g 6500 2dom 6512 xpdom2 6537 dom0 6544 phplem4dom 6568 isinfinf 6603 infm 6610 updjudhcoinlf 6761 updjudhcoinrg 6762 casef1 6771 djudom 6777 fihashf1rn 10185 |
Copyright terms: Public domain | W3C validator |