![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coeq1d | Structured version Visualization version Unicode version |
Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
Ref | Expression |
---|---|
coeq1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
coeq1d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coeq1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | coeq1 4997 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
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: coeq12d 5004 fcof1oinvd 6209 domss2 7749 mapen 7754 mapfien 7939 hashfacen 12658 relexpsucnnr 13165 relexpsucr 13169 relexpsucnnl 13172 relexpaddnn 13191 imasval 15489 imasvalOLD 15490 cofuass 15872 cofulid 15873 setcinv 16063 catcisolem 16079 catciso 16080 yonedalem3b 16242 gsumvalx 16591 frmdup3lem 16728 symggrp 17119 f1omvdco2 17167 symggen 17189 psgnunilem1 17212 gsumval3 17619 gsumzf1o 17624 psrass1lem 18678 coe1add 18934 evls1fval 18985 evl1sca 18999 evl1var 19001 evls1var 19003 pf1mpf 19017 pf1ind 19020 znval 19183 znle2 19201 tchds 22283 dvnfval 22955 hocsubdir 27519 fcoinver 28290 fcobij 28385 symgfcoeu 28682 subfacp1lem5 29979 mrsubffval 30217 mrsubfval 30218 mrsubrn 30223 elmrsubrn 30230 upixp 32120 ltrncoidN 33764 trlcoat 34361 trlcone 34366 cdlemg47a 34372 cdlemg47 34374 ltrnco4 34377 tendovalco 34403 tendoplcbv 34413 tendopl 34414 tendoplass 34421 tendo0pl 34429 tendoipl 34435 cdlemk45 34585 cdlemk53b 34594 cdlemk55a 34597 erngdvlem3 34628 erngdvlem3-rN 34636 tendocnv 34660 dvhvaddcbv 34728 dvhvaddval 34729 dvhvaddass 34736 dicvscacl 34830 cdlemn8 34843 dihordlem7b 34854 dihopelvalcpre 34887 relexp2 36340 relexpxpnnidm 36366 relexpiidm 36367 relexpmulnn 36372 relexpaddss 36381 trclfvcom 36386 trclfvdecomr 36391 frege131d 36427 |
Copyright terms: Public domain | W3C validator |