Theorem coeq2 5801

Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)

Assertion

Ref	Expression
coeq2	⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Proof of Theorem coeq2

Step	Hyp	Ref	Expression
1		coss2 5799	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
2		coss2 5799	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴))
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
4		eqss 3951	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3951	. 2 ⊢ ((𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) ↔ ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3903   ∘ ccom 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3920  df-br 5093  df-opab 5155  df-co 5628

This theorem is referenced by:  coeq2i  5803  coeq2d  5805  coi2  6212  f1eqcocnv  7238  ereq1  8632  dfttrcl2  9620  seqf1olem2  13949  seqf1o  13950  relexpsucnnr  14932  isps  18474  pwsco2mhm  18707  gsumwmhm  18719  frmdgsum  18736  frmdup1  18738  frmdup2  18739  efmndov  18755  symggrplem  18758  smndex1mndlem  18783  smndex1mnd  18784  pmtr3ncom  19354  psgnunilem1  19372  frgpuplem  19651  frgpupf  19652  frgpupval  19653  gsumval3eu  19783  gsumval3lem2  19785  rngcinv  20522  ringcinv  20556  selvval  22020  rhmmpl  22268  rhmply1vr1  22272  rhmply1vsca  22273  kgencn2  23442  upxp  23508  uptx  23510  txcn  23511  xkococnlem  23544  xkococn  23545  cnmptk1  23566  cnmptkk  23568  xkofvcn  23569  imasdsf1olem  24259  pi1cof  24957  pi1coval  24958  elovolmr  25375  ovoliunlem3  25403  ismbf1  25523  motplusg  28487  hocsubdir  31729  hoddi  31934  lnopco0i  31948  opsqrlem1  32084  pjsdi2i  32101  pjin2i  32137  pjclem1  32139  symgfcoeu  33024  1arithidomlem1  33472  1arithidom  33474  mplvrpmfgalem  33545  mplvrpmga  33546  eulerpartgbij  34340  cvmliftmo  35261  cvmliftlem14  35274  cvmliftiota  35278  cvmlift2lem13  35292  cvmlift2  35293  cvmliftphtlem  35294  cvmlift3lem2  35297  cvmlift3lem6  35301  cvmlift3lem7  35302  cvmlift3lem9  35304  cvmlift3  35305  msubco  35508  ftc1anclem8  37684  upixp  37713  coideq  38225  xrneq1  38353  xrneq2  38356  trlcoat  40706  trljco  40723  tgrpov  40731  tendovalco  40748  erngmul  40789  erngmul-rN  40797  dvamulr  40995  dvavadd  40998  dvhmulr  41069  dihjatcclem4  41404  rhmpsr  42529  mendmulr  43161  hoiprodcl2  46540  ovnlecvr  46543  ovncvrrp  46549  ovnsubaddlem2  46556  ovncvr2  46596  opnvonmbllem1  46617  opnvonmbl  46619  ovolval4lem2  46635  ovolval5lem2  46638  ovolval5lem3  46639  ovolval5  46640  ovnovollem2  46642  rngcinvALTV  48264  ringcinvALTV  48298  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsucov  48657