![]() |
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 4991 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | coss2 4991 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anim12i 570 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eqss 3447 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqss 3447 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3imtr4i 270 |
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-or 372 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-nfc 2581 df-in 3411 df-ss 3418 df-br 4403 df-opab 4462 df-co 4843 |
This theorem is referenced by: coeq2i 4995 coeq2d 4997 coi2 5352 relcnvtr 5355 relcoi1OLD 5365 f1eqcocnv 6199 ereq1 7370 seqf1olem2 12253 seqf1o 12254 relexpsucnnr 13088 isps 16448 pwsco2mhm 16618 gsumwmhm 16629 frmdgsum 16646 frmdup1 16648 frmdup2 16649 symgov 17031 pmtr3ncom 17116 psgnunilem1 17134 frgpuplem 17422 frgpupf 17423 frgpupval 17424 gsumval3eu 17538 gsumval3lem2 17540 kgencn2 20572 upxp 20638 uptx 20640 txcn 20641 xkococnlem 20674 xkococn 20675 cnmptk1 20696 cnmptkk 20698 xkofvcn 20699 imasdsf1olem 21388 pi1cof 22090 pi1coval 22091 elovolmr 22429 ovoliunlem3 22457 ismbf1 22582 motplusg 24587 hocsubdir 27438 hoddi 27643 lnopco0i 27657 opsqrlem1 27793 pjsdi2i 27810 pjin2i 27846 pjclem1 27848 symgfcoeu 28608 eulerpartgbij 29205 cvmliftmo 30007 cvmliftlem14 30020 cvmliftiota 30024 cvmlift2lem13 30038 cvmlift2 30039 cvmliftphtlem 30040 cvmlift3lem2 30043 cvmlift3lem6 30047 cvmlift3lem7 30048 cvmlift3lem9 30050 cvmlift3 30051 msubco 30169 ftc1anclem8 32024 upixp 32056 trlcoat 34290 trljco 34307 tgrpov 34315 tendovalco 34332 erngmul 34373 erngmul-rN 34381 dvamulr 34579 dvavadd 34582 dvhmulr 34654 dihjatcclem4 34989 mendmulr 36054 hoiprodcl2 38377 ovnlecvr 38380 ovncvrrp 38386 ovnsubaddlem2 38393 ovncvr2 38433 opnvonmbllem1 38454 opnvonmbl 38456 rngcinv 40036 rngcinvALTV 40048 ringcinv 40087 ringcinvALTV 40111 |
Copyright terms: Public domain | W3C validator |