Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > coeq12d | Structured version Visualization version Unicode version |
Description: Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
Ref | Expression |
---|---|
coeq12d.1 | |
coeq12d.2 |
Ref | Expression |
---|---|
coeq12d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coeq12d.1 | . . 3 | |
2 | 1 | coeq1d 5283 | . 2 |
3 | coeq12d.2 | . . 3 | |
4 | 3 | coeq2d 5284 | . 2 |
5 | 2, 4 | eqtrd 2656 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 ccom 5118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-in 3581 df-ss 3588 df-br 4654 df-opab 4713 df-co 5123 |
This theorem is referenced by: xpcoid 5676 dfac12lem1 8965 dfac12r 8968 trcleq2lem 13730 trclfvcotrg 13757 relexpaddg 13793 dfrtrcl2 13802 imasval 16171 cofuval 16542 cofu2nd 16545 cofuval2 16547 cofuass 16549 cofurid 16551 setcco 16733 estrcco 16770 funcestrcsetclem9 16788 funcsetcestrclem9 16803 isdir 17232 evl1fval 19692 znval 19883 znle2 19902 mdetfval 20392 mdetdiaglem 20404 ust0 22023 trust 22033 metustexhalf 22361 isngp 22400 ngppropd 22441 tngval 22443 tngngp2 22456 imsval 27540 opsqrlem3 29001 hmopidmch 29012 hmopidmpj 29013 pjidmco 29040 dfpjop 29041 zhmnrg 30011 istendo 36048 tendoco2 36056 tendoidcl 36057 tendococl 36060 tendoplcbv 36063 tendopl2 36065 tendoplco2 36067 tendodi1 36072 tendodi2 36073 tendo0co2 36076 tendoicl 36084 erngplus2 36092 erngplus2-rN 36100 cdlemk55u1 36253 cdlemk55u 36254 dvaplusgv 36298 dvhopvadd 36382 dvhlveclem 36397 dvhopaddN 36403 dicvaddcl 36479 dihopelvalcpre 36537 rtrclex 37924 trclubgNEW 37925 rtrclexi 37928 cnvtrcl0 37933 dfrtrcl5 37936 trcleq2lemRP 37937 csbcog 37941 trrelind 37957 trrelsuperreldg 37960 trficl 37961 trrelsuperrel2dg 37963 trclrelexplem 38003 relexpaddss 38010 dfrtrcl3 38025 clsneicnv 38403 neicvgnvo 38413 rngccoALTV 41988 funcrngcsetcALT 41999 funcringcsetcALTV2lem9 42044 ringccoALTV 42051 funcringcsetclem9ALTV 42067 |
Copyright terms: Public domain | W3C validator |