Theorem coeq2 5712

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ⊆ wss 3853   ∘ ccom 5540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-br 5040  df-opab 5102  df-co 5545

This theorem is referenced by:  coeq2i  5714  coeq2d  5716  coi2  6107  f1eqcocnv  7089  f1eqcocnvOLD  7090  ereq1  8376  seqf1olem2  13581  seqf1o  13582  relexpsucnnr  14553  isps  18028  pwsco2mhm  18213  gsumwmhm  18226  frmdgsum  18243  frmdup1  18245  frmdup2  18246  efmndov  18262  symggrplem  18265  smndex1mndlem  18290  smndex1mnd  18291  pmtr3ncom  18821  psgnunilem1  18839  frgpuplem  19116  frgpupf  19117  frgpupval  19118  gsumval3eu  19243  gsumval3lem2  19245  selvval  21032  kgencn2  22408  upxp  22474  uptx  22476  txcn  22477  xkococnlem  22510  xkococn  22511  cnmptk1  22532  cnmptkk  22534  xkofvcn  22535  imasdsf1olem  23225  pi1cof  23910  pi1coval  23911  elovolmr  24327  ovoliunlem3  24355  ismbf1  24475  motplusg  26587  hocsubdir  29820  hoddi  30025  lnopco0i  30039  opsqrlem1  30175  pjsdi2i  30192  pjin2i  30228  pjclem1  30230  symgfcoeu  31024  eulerpartgbij  32005  cvmliftmo  32913  cvmliftlem14  32926  cvmliftiota  32930  cvmlift2lem13  32944  cvmlift2  32945  cvmliftphtlem  32946  cvmlift3lem2  32949  cvmlift3lem6  32953  cvmlift3lem7  32954  cvmlift3lem9  32956  cvmlift3  32957  msubco  33160  ftc1anclem8  35543  upixp  35573  coideq  36071  xrneq1  36193  xrneq2  36196  trlcoat  38423  trljco  38440  tgrpov  38448  tendovalco  38465  erngmul  38506  erngmul-rN  38514  dvamulr  38712  dvavadd  38715  dvhmulr  38786  dihjatcclem4  39121  mendmulr  40657  hoiprodcl2  43711  ovnlecvr  43714  ovncvrrp  43720  ovnsubaddlem2  43727  ovncvr2  43767  opnvonmbllem1  43788  opnvonmbl  43790  ovolval4lem2  43806  ovolval5lem2  43809  ovolval5lem3  43810  ovolval5  43811  ovnovollem2  43813  rngcinv  45155  rngcinvALTV  45167  ringcinv  45206  ringcinvALTV  45230  itcoval1  45625  itcoval2  45626  itcoval3  45627  itcovalsucov  45630