Theorem coeq2 5825

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3917   ∘ ccom 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-co 5650

This theorem is referenced by:  coeq2i  5827  coeq2d  5829  coi2  6239  f1eqcocnv  7279  ereq1  8681  dfttrcl2  9684  seqf1olem2  14014  seqf1o  14015  relexpsucnnr  14998  isps  18534  pwsco2mhm  18767  gsumwmhm  18779  frmdgsum  18796  frmdup1  18798  frmdup2  18799  efmndov  18815  symggrplem  18818  smndex1mndlem  18843  smndex1mnd  18844  pmtr3ncom  19412  psgnunilem1  19430  frgpuplem  19709  frgpupf  19710  frgpupval  19711  gsumval3eu  19841  gsumval3lem2  19843  rngcinv  20553  ringcinv  20587  selvval  22029  rhmmpl  22277  rhmply1vr1  22281  rhmply1vsca  22282  kgencn2  23451  upxp  23517  uptx  23519  txcn  23520  xkococnlem  23553  xkococn  23554  cnmptk1  23575  cnmptkk  23577  xkofvcn  23578  imasdsf1olem  24268  pi1cof  24966  pi1coval  24967  elovolmr  25384  ovoliunlem3  25412  ismbf1  25532  motplusg  28476  hocsubdir  31721  hoddi  31926  lnopco0i  31940  opsqrlem1  32076  pjsdi2i  32093  pjin2i  32129  pjclem1  32131  symgfcoeu  33046  1arithidomlem1  33513  1arithidom  33515  eulerpartgbij  34370  cvmliftmo  35278  cvmliftlem14  35291  cvmliftiota  35295  cvmlift2lem13  35309  cvmlift2  35310  cvmliftphtlem  35311  cvmlift3lem2  35314  cvmlift3lem6  35318  cvmlift3lem7  35319  cvmlift3lem9  35321  cvmlift3  35322  msubco  35525  ftc1anclem8  37701  upixp  37730  coideq  38242  xrneq1  38370  xrneq2  38373  trlcoat  40724  trljco  40741  tgrpov  40749  tendovalco  40766  erngmul  40807  erngmul-rN  40815  dvamulr  41013  dvavadd  41016  dvhmulr  41087  dihjatcclem4  41422  rhmpsr  42547  mendmulr  43180  hoiprodcl2  46560  ovnlecvr  46563  ovncvrrp  46569  ovnsubaddlem2  46576  ovncvr2  46616  opnvonmbllem1  46637  opnvonmbl  46639  ovolval4lem2  46655  ovolval5lem2  46658  ovolval5lem3  46659  ovolval5  46660  ovnovollem2  46662  rngcinvALTV  48268  ringcinvALTV  48302  itcoval1  48656  itcoval2  48657  itcoval3  48658  itcovalsucov  48661