Theorem coeq2 5767

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 5765	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
2		coss2 5765	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴))
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
4		eqss 3936	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3936	. 2 ⊢ ((𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) ↔ ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ⊆ wss 3887   ∘ ccom 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-br 5075  df-opab 5137  df-co 5598

This theorem is referenced by:  coeq2i  5769  coeq2d  5771  coi2  6167  f1eqcocnv  7173  f1eqcocnvOLD  7174  ereq1  8505  dfttrcl2  9482  seqf1olem2  13763  seqf1o  13764  relexpsucnnr  14736  isps  18286  pwsco2mhm  18471  gsumwmhm  18484  frmdgsum  18501  frmdup1  18503  frmdup2  18504  efmndov  18520  symggrplem  18523  smndex1mndlem  18548  smndex1mnd  18549  pmtr3ncom  19083  psgnunilem1  19101  frgpuplem  19378  frgpupf  19379  frgpupval  19380  gsumval3eu  19505  gsumval3lem2  19507  selvval  21328  kgencn2  22708  upxp  22774  uptx  22776  txcn  22777  xkococnlem  22810  xkococn  22811  cnmptk1  22832  cnmptkk  22834  xkofvcn  22835  imasdsf1olem  23526  pi1cof  24222  pi1coval  24223  elovolmr  24640  ovoliunlem3  24668  ismbf1  24788  motplusg  26903  hocsubdir  30147  hoddi  30352  lnopco0i  30366  opsqrlem1  30502  pjsdi2i  30519  pjin2i  30555  pjclem1  30557  symgfcoeu  31351  eulerpartgbij  32339  cvmliftmo  33246  cvmliftlem14  33259  cvmliftiota  33263  cvmlift2lem13  33277  cvmlift2  33278  cvmliftphtlem  33279  cvmlift3lem2  33282  cvmlift3lem6  33286  cvmlift3lem7  33287  cvmlift3lem9  33289  cvmlift3  33290  msubco  33493  ftc1anclem8  35857  upixp  35887  coideq  36385  xrneq1  36507  xrneq2  36510  trlcoat  38737  trljco  38754  tgrpov  38762  tendovalco  38779  erngmul  38820  erngmul-rN  38828  dvamulr  39026  dvavadd  39029  dvhmulr  39100  dihjatcclem4  39435  mendmulr  41013  hoiprodcl2  44093  ovnlecvr  44096  ovncvrrp  44102  ovnsubaddlem2  44109  ovncvr2  44149  opnvonmbllem1  44170  opnvonmbl  44172  ovolval4lem2  44188  ovolval5lem2  44191  ovolval5lem3  44192  ovolval5  44193  ovnovollem2  44195  rngcinv  45539  rngcinvALTV  45551  ringcinv  45590  ringcinvALTV  45614  itcoval1  46009  itcoval2  46010  itcoval3  46011  itcovalsucov  46014