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  18509  pwsco2mhm  18742  gsumwmhm  18754  frmdgsum  18771  frmdup1  18773  frmdup2  18774  efmndov  18790  symggrplem  18793  smndex1mndlem  18818  smndex1mnd  18819  pmtr3ncom  19389  psgnunilem1  19407  frgpuplem  19686  frgpupf  19687  frgpupval  19688  gsumval3eu  19818  gsumval3lem2  19820  rngcinv  20557  ringcinv  20591  selvval  22055  rhmmpl  22303  rhmply1vr1  22307  rhmply1vsca  22308  kgencn2  23477  upxp  23543  uptx  23545  txcn  23546  xkococnlem  23579  xkococn  23580  cnmptk1  23601  cnmptkk  23603  xkofvcn  23604  imasdsf1olem  24294  pi1cof  24992  pi1coval  24993  elovolmr  25410  ovoliunlem3  25438  ismbf1  25558  motplusg  28522  hocsubdir  31764  hoddi  31969  lnopco0i  31983  opsqrlem1  32119  pjsdi2i  32136  pjin2i  32172  pjclem1  32174  symgfcoeu  33054  1arithidomlem1  33499  1arithidom  33501  eulerpartgbij  34356  cvmliftmo  35264  cvmliftlem14  35277  cvmliftiota  35281  cvmlift2lem13  35295  cvmlift2  35296  cvmliftphtlem  35297  cvmlift3lem2  35300  cvmlift3lem6  35304  cvmlift3lem7  35305  cvmlift3lem9  35307  cvmlift3  35308  msubco  35511  ftc1anclem8  37687  upixp  37716  coideq  38228  xrneq1  38356  xrneq2  38359  trlcoat  40710  trljco  40727  tgrpov  40735  tendovalco  40752  erngmul  40793  erngmul-rN  40801  dvamulr  40999  dvavadd  41002  dvhmulr  41073  dihjatcclem4  41408  rhmpsr  42533  mendmulr  43166  hoiprodcl2  46546  ovnlecvr  46549  ovncvrrp  46555  ovnsubaddlem2  46562  ovncvr2  46602  opnvonmbllem1  46623  opnvonmbl  46625  ovolval4lem2  46641  ovolval5lem2  46644  ovolval5lem3  46645  ovolval5  46646  ovnovollem2  46648  rngcinvALTV  48257  ringcinvALTV  48291  itcoval1  48645  itcoval2  48646  itcoval3  48647  itcovalsucov  48650