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

Theorem coeq1d 5439
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 5435 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  ccom 5270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-in 3722  df-ss 3729  df-br 4805  df-opab 4865  df-co 5275
This theorem is referenced by:  coeq12d  5442  fcof1oinvd  6712  domss2  8286  mapen  8291  mapfien  8480  hashfacen  13450  relexpsucnnr  13984  relexpsucr  13988  relexpsucnnl  13991  relexpaddnn  14010  imasval  16393  cofuass  16770  cofulid  16771  setcinv  16961  catcisolem  16977  catciso  16978  yonedalem3b  17140  gsumvalx  17491  frmdup3lem  17624  symggrp  18040  f1omvdco2  18088  symggen  18110  psgnunilem1  18133  gsumval3  18528  gsumzf1o  18533  psrass1lem  19599  coe1add  19856  evls1fval  19906  evl1sca  19920  evl1var  19922  evls1var  19924  pf1mpf  19938  pf1ind  19941  znval  20105  znle2  20124  tchds  23250  dvnfval  23904  hocsubdir  28974  fcoinver  29746  fcobij  29830  symgfcoeu  30175  reprpmtf1o  31034  hgt750lemg  31062  subfacp1lem5  31494  mrsubffval  31732  mrsubfval  31733  mrsubrn  31738  elmrsubrn  31745  upixp  33855  ltrncoidN  35935  trlcoat  36531  trlcone  36536  cdlemg47a  36542  cdlemg47  36544  ltrnco4  36547  tendovalco  36573  tendoplcbv  36583  tendopl  36584  tendoplass  36591  tendo0pl  36599  tendoipl  36605  cdlemk45  36755  cdlemk53b  36764  cdlemk55a  36767  erngdvlem3  36798  erngdvlem3-rN  36806  tendocnv  36830  dvhvaddcbv  36898  dvhvaddval  36899  dvhvaddass  36906  dicvscacl  37000  cdlemn8  37013  dihordlem7b  37024  dihopelvalcpre  37057  relexp2  38489  relexpxpnnidm  38515  relexpiidm  38516  relexpmulnn  38521  relexpaddss  38530  trclfvcom  38535  trclfvdecomr  38540  frege131d  38576  dssmap2d  38836
  Copyright terms: Public domain W3C validator