![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-f1o | Structured version Visualization version Unicode version |
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5842, dff1o3 5843, dff1o4 5845, and dff1o5 5846. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f1o |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cF |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | wf1o 5600 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 3 | wf1 5598 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 3 | wfo 5599 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
7 | 5, 6 | wa 375 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | wb 189 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: f1oeq1 5828 f1oeq2 5829 f1oeq3 5830 nff1o 5835 f1of1 5836 dff1o2 5842 dff1o5 5846 f1oco 5859 fo00 5871 dff1o6 6199 nvof1o 6204 fcof1od 6217 soisoi 6244 f1oweALT 6804 tposf1o2 7025 smoiso2 7114 f1finf1o 7824 unfilem2 7862 fofinf1o 7878 alephiso 8555 cnref1o 11326 wwlktovf1o 13083 1arith 14920 xpsff1o 15523 isffth2 15870 ffthf1o 15873 orbsta 17016 symgextf1o 17113 symgfixf1o 17130 odf1o1 17270 znf1o 19171 cygznlem3 19189 scmatf1o 19606 m2cpmf1o 19830 pm2mpf1o 19888 reeff1o 23451 recosf1o 23533 efif1olem4 23543 dvdsmulf1o 24172 wlknwwlknbij 25490 wlkiswwlkbij 25497 wwlkextbij0 25509 clwwlkf1o 25575 clwlkf1oclwwlk 25628 eupatrl 25745 frgrancvvdeqlem8 25817 numclwlk1lem2f1o 25873 unopf1o 27618 ghomf1olem 30361 poimirlem26 32011 poimirlem27 32012 wessf1ornlem 37497 projf1o 37512 sumnnodd 37748 dvnprodlem1 37859 fourierdlem54 38062 |
Copyright terms: Public domain | W3C validator |