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  33025  1arithidomlem1  33473  1arithidom  33475  mplvrpmfgalem  33547  mplvrpmga  33548  mplvrpmmhm  33549  eulerpartgbij  34346  cvmliftmo  35267  cvmliftlem14  35280  cvmliftiota  35284  cvmlift2lem13  35298  cvmlift2  35299  cvmliftphtlem  35300  cvmlift3lem2  35303  cvmlift3lem6  35307  cvmlift3lem7  35308  cvmlift3lem9  35310  cvmlift3  35311  msubco  35514  ftc1anclem8  37690  upixp  37719  coideq  38231  xrneq1  38359  xrneq2  38362  trlcoat  40712  trljco  40729  tgrpov  40737  tendovalco  40754  erngmul  40795  erngmul-rN  40803  dvamulr  41001  dvavadd  41004  dvhmulr  41075  dihjatcclem4  41410  rhmpsr  42535  mendmulr  43167  hoiprodcl2  46546  ovnlecvr  46549  ovncvrrp  46555  ovnsubaddlem2  46562  ovncvr2  46602  opnvonmbllem1  46623  opnvonmbl  46625  ovolval4lem2  46641  ovolval5lem2  46644  ovolval5lem3  46645  ovolval5  46646  ovnovollem2  46648  rngcinvALTV  48270  ringcinvALTV  48304  itcoval1  48658  itcoval2  48659  itcoval3  48660  itcovalsucov  48663