![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1oeq3 | Structured version Visualization version Unicode version |
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1oeq3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1eq3 5776 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | foeq3 5791 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anbi12d 717 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-f1o 5589 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-f1o 5589 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3bitr4g 292 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-in 3411 df-ss 3418 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 |
This theorem is referenced by: f1oeq23 5808 f1oeq123d 5811 f1ores 5828 resdif 5834 resin 5835 f1osng 5853 f1oresrab 6055 fveqf1o 6200 isoeq5 6214 isoini2 6230 ncanth 6250 oacomf1o 7266 mapsnf1o 7563 bren 7578 xpcomf1o 7661 domss2 7731 isinf 7785 wemapwe 8202 oef1o 8203 cnfcomlem 8204 cnfcom2 8207 cnfcom3 8209 cnfcom3clem 8210 infxpenc 8449 infxpenc2lem1 8450 infxpenc2 8453 ackbij2lem2 8670 fin1a2lem6 8835 hsmexlem1 8856 pwfseqlem5 9088 pwfseq 9089 hashgf1o 12184 axdc4uzlem 12195 sumeq1 13755 fsumss 13791 fsumcnv 13834 prodeq1f 13962 fprodss 14002 fprodcnv 14037 unbenlem 14852 4sqlem11 14899 pwssnf1o 15396 catcisolem 16001 equivestrcsetc 16037 yoniso 16170 gsumvalx 16513 gsumpropd 16515 gsumpropd2lem 16516 xpsmnd 16576 xpsgrp 16805 cayley 17055 cayleyth 17056 gsumval3lem1 17539 gsumval3lem2 17540 gsumcom2 17607 coe1mul2lem2 18861 scmatrngiso 19561 m2cpmrngiso 19782 cncfcnvcn 21953 ovolicc2lem4OLD 22473 ovolicc2lem4 22474 logf1o2 23595 uslgraf1oedg 25086 clwwlkvbij 25529 iseupa 25693 adjbd1o 27738 rinvf1o 28230 eulerpartgbij 29205 eulerpartlemgh 29211 derangval 29890 subfacp1lem2a 29903 subfacp1lem3 29905 subfacp1lem5 29907 mrsubff1o 30153 msubff1o 30195 elgiso 30314 bj-finsumval0 31702 f1omptsnlem 31738 f1omptsn 31739 poimirlem4 31944 poimirlem9 31949 poimirlem15 31955 ismtyval 32132 ismrer1 32170 rngoisoval 32216 lautset 33647 pautsetN 33663 hvmap1o2 35333 pwfi2f1o 35954 imasgim 35958 f1oeq3d 37442 uspgrf1oedg 39260 usgrf1oedg 39290 |
Copyright terms: Public domain | W3C validator |