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 4907 | . 2 | |
2 | 1 | simplbi 259 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 ccnv 4344 wfun 4896 wf 4898 wf1 4899 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 df-f1 4907 |
This theorem is referenced by: f1fn 5093 f1ss 5097 f1ssres 5099 f1of 5126 dff1o5 5135 fun11iun 5147 cocan1 5427 f1dmex 5743 f1o2ndf1 5849 brdomg 6229 f1dom2g 6236 f1domg 6238 dom3d 6254 f1imaen2g 6273 2dom 6285 xpdom2 6305 phplem4dom 6324 |
Copyright terms: Public domain | W3C validator |