MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coeq1d Unicode version

Theorem coeq1d 5005
Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
Hypothesis
Ref Expression
coeq1d.1
Assertion
Ref Expression
coeq1d

Proof of Theorem coeq1d
StepHypRef Expression
1 coeq1d.1 . 2
2 coeq1 5001 . 2
31, 2syl 16 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1662  o.ccom 4848
This theorem is referenced by:  coeq12d  5008  fcof1o  5971  domss2  7378  mapen  7383  mapfien  7765  hashfacen  11994  imasval  14228  cofuass  14577  cofulid  14578  setcinv  14736  catcisolem  14752  catciso  14753  yonedalem3b  14867  gsumvalx  15277  frmdup3  15314  symggrp  15606  gsumval3  16017  gsumzf1o  16022  psrass1lem  16945  coe1add  17160  znval  17319  znle2  17337  dvnfval  20312  evl1sca  20454  evl1var  20456  pf1mpf  20476  pf1ind  20479  hocsubdir  23799  fcobij  24646  subfacp1lem5  25709  relexpsucr  25963  relexpsucl  25965  relexpcnv  25966  relexpadd  25971  upixp  27294  f1omvdco2  28297  symggen  28317  psgnunilem1  28322  ltrncoidN  32198  trlcoat  32793  trlcone  32798  cdlemg47a  32804  cdlemg47  32806  ltrnco4  32809  tendovalco  32835  tendoplcbv  32845  tendopl  32846  tendoplass  32853  tendo0pl  32861  tendoipl  32867  cdlemk45  33017  cdlemk53b  33026  cdlemk55a  33029  erngdvlem3  33060  erngdvlem3-rN  33068  tendocnv  33092  dvhvaddcbv  33160  dvhvaddval  33161  dvhvaddass  33168  dicvscacl  33262  cdlemn8  33275  dihordlem7b  33286  dihopelvalcpre  33319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-in 3360  df-ss 3367  df-br 4303  df-opab 4361  df-co 4853
  Copyright terms: Public domain W3C validator