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

Theorem coeq1d 5731
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 5727 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  ccom 5558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-in 3947  df-ss 3956  df-br 5064  df-opab 5126  df-co 5563
This theorem is referenced by:  coeq12d  5734  fcof1oinvd  7045  domss2  8670  mapen  8675  mapfien  8865  hashfacen  13807  relexpsucnnr  14379  relexpsucr  14383  relexpsucnnl  14386  relexpaddnn  14405  imasval  16779  cofuass  17154  cofulid  17155  setcinv  17345  catcisolem  17361  catciso  17362  yonedalem3b  17524  gsumvalx  17881  frmdup3lem  18026  symggrplem  18463  f1omvdco2  18512  symggen  18534  psgnunilem1  18557  gsumval3  18963  gsumzf1o  18968  psrass1lem  20092  coe1add  20367  evls1fval  20417  evl1sca  20432  evl1var  20434  evls1var  20436  pf1mpf  20450  pf1ind  20453  znval  20617  znle2  20635  tcphds  23768  dvnfval  24453  hocsubdir  29495  fcoinver  30291  fcobij  30390  symgfcoeu  30659  symgcom  30660  pmtrcnel2  30667  tocyc01  30693  cycpm2tr  30694  cycpmconjv  30717  cycpmconjslem1  30729  cycpmconjslem2  30730  cycpmconjs  30731  cyc3conja  30732  reprpmtf1o  31802  hgt750lemg  31830  subfacp1lem5  32334  mrsubffval  32657  mrsubfval  32658  mrsubrn  32663  elmrsubrn  32670  upixp  34891  ltrncoidN  37150  trlcoat  37745  trlcone  37750  cdlemg47a  37756  cdlemg47  37758  ltrnco4  37761  tendovalco  37787  tendoplcbv  37797  tendopl  37798  tendoplass  37805  tendo0pl  37813  tendoipl  37819  cdlemk45  37969  cdlemk53b  37978  cdlemk55a  37981  erngdvlem3  38012  erngdvlem3-rN  38020  tendocnv  38043  dvhvaddcbv  38111  dvhvaddval  38112  dvhvaddass  38119  dicvscacl  38213  cdlemn8  38226  dihordlem7b  38237  dihopelvalcpre  38270  relexp2  39906  relexpxpnnidm  39932  relexpiidm  39933  relexpmulnn  39938  relexpaddss  39947  trclfvcom  39952  trclfvdecomr  39957  frege131d  39993  dssmap2d  40252  isomushgr  43842
  Copyright terms: Public domain W3C validator