Theorem coeq2 5856

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ⊆ wss 3947   ∘ ccom 5679

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-br 5148  df-opab 5210  df-co 5684

This theorem is referenced by:  coeq2i  5858  coeq2d  5860  coi2  6259  f1eqcocnv  7295  f1eqcocnvOLD  7296  ereq1  8706  dfttrcl2  9715  seqf1olem2  14004  seqf1o  14005  relexpsucnnr  14968  isps  18517  pwsco2mhm  18710  gsumwmhm  18722  frmdgsum  18739  frmdup1  18741  frmdup2  18742  efmndov  18758  symggrplem  18761  smndex1mndlem  18786  smndex1mnd  18787  pmtr3ncom  19337  psgnunilem1  19355  frgpuplem  19634  frgpupf  19635  frgpupval  19636  gsumval3eu  19766  gsumval3lem2  19768  selvval  21672  kgencn2  23052  upxp  23118  uptx  23120  txcn  23121  xkococnlem  23154  xkococn  23155  cnmptk1  23176  cnmptkk  23178  xkofvcn  23179  imasdsf1olem  23870  pi1cof  24566  pi1coval  24567  elovolmr  24984  ovoliunlem3  25012  ismbf1  25132  motplusg  27782  hocsubdir  31025  hoddi  31230  lnopco0i  31244  opsqrlem1  31380  pjsdi2i  31397  pjin2i  31433  pjclem1  31435  symgfcoeu  32230  eulerpartgbij  33359  cvmliftmo  34263  cvmliftlem14  34276  cvmliftiota  34280  cvmlift2lem13  34294  cvmlift2  34295  cvmliftphtlem  34296  cvmlift3lem2  34299  cvmlift3lem6  34303  cvmlift3lem7  34304  cvmlift3lem9  34306  cvmlift3  34307  msubco  34510  ftc1anclem8  36556  upixp  36585  coideq  37101  xrneq1  37235  xrneq2  37238  trlcoat  39582  trljco  39599  tgrpov  39607  tendovalco  39624  erngmul  39665  erngmul-rN  39673  dvamulr  39871  dvavadd  39874  dvhmulr  39945  dihjatcclem4  40280  rhmmpl  41122  mendmulr  41915  hoiprodcl2  45257  ovnlecvr  45260  ovncvrrp  45266  ovnsubaddlem2  45273  ovncvr2  45313  opnvonmbllem1  45334  opnvonmbl  45336  ovolval4lem2  45352  ovolval5lem2  45355  ovolval5lem3  45356  ovolval5  45357  ovnovollem2  45359  rngcinv  46832  rngcinvALTV  46844  ringcinv  46883  ringcinvALTV  46907  itcoval1  47302  itcoval2  47303  itcoval3  47304  itcovalsucov  47307