Theorem coeq2 5859

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ⊆ wss 3949   ∘ ccom 5681

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-co 5686

This theorem is referenced by:  coeq2i  5861  coeq2d  5863  coi2  6263  f1eqcocnv  7299  f1eqcocnvOLD  7300  ereq1  8710  dfttrcl2  9719  seqf1olem2  14008  seqf1o  14009  relexpsucnnr  14972  isps  18521  pwsco2mhm  18714  gsumwmhm  18726  frmdgsum  18743  frmdup1  18745  frmdup2  18746  efmndov  18762  symggrplem  18765  smndex1mndlem  18790  smndex1mnd  18791  pmtr3ncom  19343  psgnunilem1  19361  frgpuplem  19640  frgpupf  19641  frgpupval  19642  gsumval3eu  19772  gsumval3lem2  19774  selvval  21681  kgencn2  23061  upxp  23127  uptx  23129  txcn  23130  xkococnlem  23163  xkococn  23164  cnmptk1  23185  cnmptkk  23187  xkofvcn  23188  imasdsf1olem  23879  pi1cof  24575  pi1coval  24576  elovolmr  24993  ovoliunlem3  25021  ismbf1  25141  motplusg  27793  hocsubdir  31038  hoddi  31243  lnopco0i  31257  opsqrlem1  31393  pjsdi2i  31410  pjin2i  31446  pjclem1  31448  symgfcoeu  32243  eulerpartgbij  33371  cvmliftmo  34275  cvmliftlem14  34288  cvmliftiota  34292  cvmlift2lem13  34306  cvmlift2  34307  cvmliftphtlem  34308  cvmlift3lem2  34311  cvmlift3lem6  34315  cvmlift3lem7  34316  cvmlift3lem9  34318  cvmlift3  34319  msubco  34522  ftc1anclem8  36568  upixp  36597  coideq  37113  xrneq1  37247  xrneq2  37250  trlcoat  39594  trljco  39611  tgrpov  39619  tendovalco  39636  erngmul  39677  erngmul-rN  39685  dvamulr  39883  dvavadd  39886  dvhmulr  39957  dihjatcclem4  40292  rhmmpl  41125  mendmulr  41930  hoiprodcl2  45271  ovnlecvr  45274  ovncvrrp  45280  ovnsubaddlem2  45287  ovncvr2  45327  opnvonmbllem1  45348  opnvonmbl  45350  ovolval4lem2  45366  ovolval5lem2  45369  ovolval5lem3  45370  ovolval5  45371  ovnovollem2  45373  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954  itcoval1  47349  itcoval2  47350  itcoval3  47351  itcovalsucov  47354