Theorem coeq2 5756

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3883   ∘ ccom 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-co 5589

This theorem is referenced by:  coeq2i  5758  coeq2d  5760  coi2  6156  f1eqcocnv  7153  f1eqcocnvOLD  7154  ereq1  8463  seqf1olem2  13691  seqf1o  13692  relexpsucnnr  14664  isps  18201  pwsco2mhm  18386  gsumwmhm  18399  frmdgsum  18416  frmdup1  18418  frmdup2  18419  efmndov  18435  symggrplem  18438  smndex1mndlem  18463  smndex1mnd  18464  pmtr3ncom  18998  psgnunilem1  19016  frgpuplem  19293  frgpupf  19294  frgpupval  19295  gsumval3eu  19420  gsumval3lem2  19422  selvval  21238  kgencn2  22616  upxp  22682  uptx  22684  txcn  22685  xkococnlem  22718  xkococn  22719  cnmptk1  22740  cnmptkk  22742  xkofvcn  22743  imasdsf1olem  23434  pi1cof  24128  pi1coval  24129  elovolmr  24545  ovoliunlem3  24573  ismbf1  24693  motplusg  26807  hocsubdir  30048  hoddi  30253  lnopco0i  30267  opsqrlem1  30403  pjsdi2i  30420  pjin2i  30456  pjclem1  30458  symgfcoeu  31253  eulerpartgbij  32239  cvmliftmo  33146  cvmliftlem14  33159  cvmliftiota  33163  cvmlift2lem13  33177  cvmlift2  33178  cvmliftphtlem  33179  cvmlift3lem2  33182  cvmlift3lem6  33186  cvmlift3lem7  33187  cvmlift3lem9  33189  cvmlift3  33190  msubco  33393  dfttrcl2  33710  ftc1anclem8  35784  upixp  35814  coideq  36312  xrneq1  36434  xrneq2  36437  trlcoat  38664  trljco  38681  tgrpov  38689  tendovalco  38706  erngmul  38747  erngmul-rN  38755  dvamulr  38953  dvavadd  38956  dvhmulr  39027  dihjatcclem4  39362  mendmulr  40929  hoiprodcl2  43983  ovnlecvr  43986  ovncvrrp  43992  ovnsubaddlem2  43999  ovncvr2  44039  opnvonmbllem1  44060  opnvonmbl  44062  ovolval4lem2  44078  ovolval5lem2  44081  ovolval5lem3  44082  ovolval5  44083  ovnovollem2  44085  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  itcoval1  45897  itcoval2  45898  itcoval3  45899  itcovalsucov  45902