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

Theorem coeq1d 5076
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 5072 . 2
31, 2syl 16 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1654  o.ccom 4923
This theorem is referenced by:  coeq12d  5079  fcof1o  6074  domss2  7315  mapen  7320  mapfien  7702  hashfacen  11754  imasval  13788  cofuass  14137  cofulid  14138  setcinv  14296  catcisolem  14312  catciso  14313  yonedalem3b  14427  gsumvalx  14825  frmdup3  14862  symggrp  15154  gsumval3  15565  gsumzf1o  15570  psrass1lem  16493  coe1add  16708  znval  16867  znle2  16885  dvnfval  19859  evl1sca  20001  evl1var  20003  pf1mpf  20023  pf1ind  20026  hocsubdir  23339  fcobij  24720  subfacp1lem5  24974  relexpsucr  25234  relexpsucl  25236  relexpcnv  25237  relexpadd  25242  upixp  26542  f1omvdco2  27547  symggen  27567  psgnunilem1  27572  ltrncoidN  31165  trlcoat  31760  trlcone  31765  cdlemg47a  31771  cdlemg47  31773  ltrnco4  31776  tendovalco  31802  tendoplcbv  31812  tendopl  31813  tendoplass  31820  tendo0pl  31828  tendoipl  31834  cdlemk45  31984  cdlemk53b  31993  cdlemk55a  31996  erngdvlem3  32027  erngdvlem3-rN  32035  tendocnv  32059  dvhvaddcbv  32127  dvhvaddval  32128  dvhvaddass  32135  dicvscacl  32229  cdlemn8  32242  dihordlem7b  32253  dihopelvalcpre  32286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-in 3316  df-ss 3323  df-br 4244  df-opab 4302  df-co 4928
  Copyright terms: Public domain W3C validator