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 5098 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 ccnv 4508 wfun 5087 wf 5089 wf1 5090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-f1 5098 |
This theorem is referenced by: f1rn 5299 f1fn 5300 f1ss 5304 f1ssres 5307 f1of 5335 dff1o5 5344 fsnd 5378 cocan1 5656 f1o2ndf1 6093 brdomg 6610 f1dom2g 6618 f1domg 6620 dom3d 6636 f1imaen2g 6655 2dom 6667 xpdom2 6693 dom0 6700 phplem4dom 6724 isinfinf 6759 infm 6766 updjudhcoinlf 6933 updjudhcoinrg 6934 casef1 6943 djudom 6946 difinfsnlem 6952 difinfsn 6953 fihashf1rn 10503 ennnfonelemrn 11859 pwle2 13120 |
Copyright terms: Public domain | W3C validator |