![]() |
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 5240 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 274 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 5240 |
This theorem is referenced by: f1rn 5441 f1fn 5442 f1ss 5446 f1ssres 5449 f1of 5480 dff1o5 5489 fsnd 5523 cocan1 5809 f1o2ndf1 6254 brdomg 6775 f1dom2g 6783 f1domg 6785 dom3d 6801 f1imaen2g 6820 2dom 6832 xpdom2 6858 dom0 6867 phplem4dom 6891 isinfinf 6926 infm 6933 updjudhcoinlf 7110 updjudhcoinrg 7111 casef1 7120 djudom 7123 difinfsnlem 7129 difinfsn 7130 fihashf1rn 10803 ennnfonelemrn 12473 reeff1o 14671 1dom1el 15221 pwle2 15227 |
Copyright terms: Public domain | W3C validator |