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

Theorem coeq1d 5023
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 5019 . 2
31, 2syl 16 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1670  o.ccom 4866
This theorem is referenced by:  coeq12d  5026  fcof1o  6007  domss2  7431  mapen  7436  mapfien  7820  hashfacen  12054  imasval  14291  cofuass  14640  cofulid  14641  setcinv  14799  catcisolem  14815  catciso  14816  yonedalem3b  14930  gsumvalx  15342  frmdup3  15382  symggrp  15686  gsumval3  16124  gsumzf1o  16129  psrass1lem  17067  coe1add  17282  znval  17441  znle2  17459  f1omvdco2  17605  symggen  17626  psgnunilem1  17646  dvnfval  20823  evl1sca  20965  evl1var  20967  pf1mpf  20987  pf1ind  20990  hocsubdir  24311  fcobij  25155  subfacp1lem5  26218  relexpsucr  26472  relexpsucl  26474  relexpcnv  26475  relexpadd  26480  upixp  27803  ltrncoidN  32475  trlcoat  33070  trlcone  33075  cdlemg47a  33081  cdlemg47  33083  ltrnco4  33086  tendovalco  33112  tendoplcbv  33122  tendopl  33123  tendoplass  33130  tendo0pl  33138  tendoipl  33144  cdlemk45  33294  cdlemk53b  33303  cdlemk55a  33306  erngdvlem3  33337  erngdvlem3-rN  33345  tendocnv  33369  dvhvaddcbv  33437  dvhvaddval  33438  dvhvaddass  33445  dicvscacl  33539  cdlemn8  33552  dihordlem7b  33563  dihopelvalcpre  33596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-in 3372  df-ss 3379  df-br 4319  df-opab 4377  df-co 4871
  Copyright terms: Public domain W3C validator