![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coeq2 | Structured version Visualization version Unicode version |
Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
Ref | Expression |
---|---|
coeq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coss2 4996 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | coss2 4996 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anim12i 576 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eqss 3433 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqss 3433 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3imtr4i 274 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-in 3397 df-ss 3404 df-br 4396 df-opab 4455 df-co 4848 |
This theorem is referenced by: coeq2i 5000 coeq2d 5002 coi2 5359 relcnvtr 5362 relcoi1OLD 5372 f1eqcocnv 6217 ereq1 7388 seqf1olem2 12291 seqf1o 12292 relexpsucnnr 13165 isps 16526 pwsco2mhm 16696 gsumwmhm 16707 frmdgsum 16724 frmdup1 16726 frmdup2 16727 symgov 17109 pmtr3ncom 17194 psgnunilem1 17212 frgpuplem 17500 frgpupf 17501 frgpupval 17502 gsumval3eu 17616 gsumval3lem2 17618 kgencn2 20649 upxp 20715 uptx 20717 txcn 20718 xkococnlem 20751 xkococn 20752 cnmptk1 20773 cnmptkk 20775 xkofvcn 20776 imasdsf1olem 21466 pi1cof 22168 pi1coval 22169 elovolmr 22507 ovoliunlem3 22535 ismbf1 22661 motplusg 24666 hocsubdir 27519 hoddi 27724 lnopco0i 27738 opsqrlem1 27874 pjsdi2i 27891 pjin2i 27927 pjclem1 27929 symgfcoeu 28682 eulerpartgbij 29278 cvmliftmo 30079 cvmliftlem14 30092 cvmliftiota 30096 cvmlift2lem13 30110 cvmlift2 30111 cvmliftphtlem 30112 cvmlift3lem2 30115 cvmlift3lem6 30119 cvmlift3lem7 30120 cvmlift3lem9 30122 cvmlift3 30123 msubco 30241 ftc1anclem8 32088 upixp 32120 trlcoat 34361 trljco 34378 tgrpov 34386 tendovalco 34403 erngmul 34444 erngmul-rN 34452 dvamulr 34650 dvavadd 34653 dvhmulr 34725 dihjatcclem4 35060 mendmulr 36125 hoiprodcl2 38495 ovnlecvr 38498 ovncvrrp 38504 ovnsubaddlem2 38511 ovncvr2 38551 opnvonmbllem1 38572 opnvonmbl 38574 ovolval4lem2 38590 ovolval5lem2 38593 ovolval5lem3 38594 ovolval5 38595 ovnovollem2 38597 rngcinv 40491 rngcinvALTV 40503 ringcinv 40542 ringcinvALTV 40566 |
Copyright terms: Public domain | W3C validator |