Theorem coeq2 5812

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-co 5640

This theorem is referenced by:  coeq2i  5814  coeq2d  5816  coi2  6224  f1eqcocnv  7258  ereq1  8655  dfttrcl2  9653  seqf1olem2  13983  seqf1o  13984  relexpsucnnr  14967  isps  18503  pwsco2mhm  18736  gsumwmhm  18748  frmdgsum  18765  frmdup1  18767  frmdup2  18768  efmndov  18784  symggrplem  18787  smndex1mndlem  18812  smndex1mnd  18813  pmtr3ncom  19381  psgnunilem1  19399  frgpuplem  19678  frgpupf  19679  frgpupval  19680  gsumval3eu  19810  gsumval3lem2  19812  rngcinv  20522  ringcinv  20556  selvval  21998  rhmmpl  22246  rhmply1vr1  22250  rhmply1vsca  22251  kgencn2  23420  upxp  23486  uptx  23488  txcn  23489  xkococnlem  23522  xkococn  23523  cnmptk1  23544  cnmptkk  23546  xkofvcn  23547  imasdsf1olem  24237  pi1cof  24935  pi1coval  24936  elovolmr  25353  ovoliunlem3  25381  ismbf1  25501  motplusg  28445  hocsubdir  31687  hoddi  31892  lnopco0i  31906  opsqrlem1  32042  pjsdi2i  32059  pjin2i  32095  pjclem1  32097  symgfcoeu  33012  1arithidomlem1  33479  1arithidom  33481  eulerpartgbij  34336  cvmliftmo  35244  cvmliftlem14  35257  cvmliftiota  35261  cvmlift2lem13  35275  cvmlift2  35276  cvmliftphtlem  35277  cvmlift3lem2  35280  cvmlift3lem6  35284  cvmlift3lem7  35285  cvmlift3lem9  35287  cvmlift3  35288  msubco  35491  ftc1anclem8  37667  upixp  37696  coideq  38208  xrneq1  38336  xrneq2  38339  trlcoat  40690  trljco  40707  tgrpov  40715  tendovalco  40732  erngmul  40773  erngmul-rN  40781  dvamulr  40979  dvavadd  40982  dvhmulr  41053  dihjatcclem4  41388  rhmpsr  42513  mendmulr  43146  hoiprodcl2  46526  ovnlecvr  46529  ovncvrrp  46535  ovnsubaddlem2  46542  ovncvr2  46582  opnvonmbllem1  46603  opnvonmbl  46605  ovolval4lem2  46621  ovolval5lem2  46624  ovolval5lem3  46625  ovolval5  46626  ovnovollem2  46628  rngcinvALTV  48237  ringcinvALTV  48271  itcoval1  48625  itcoval2  48626  itcoval3  48627  itcovalsucov  48630