Theorem coeq2 5729

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ⊆ wss 3936   ∘ ccom 5559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-br 5067  df-opab 5129  df-co 5564

This theorem is referenced by:  coeq2i  5731  coeq2d  5733  coi2  6116  f1eqcocnv  7057  ereq1  8296  seqf1olem2  13411  seqf1o  13412  relexpsucnnr  14384  isps  17812  pwsco2mhm  17997  gsumwmhm  18010  frmdgsum  18027  frmdup1  18029  frmdup2  18030  efmndov  18046  symggrplem  18049  smndex1mndlem  18074  smndex1mnd  18075  pmtr3ncom  18603  psgnunilem1  18621  frgpuplem  18898  frgpupf  18899  frgpupval  18900  gsumval3eu  19024  gsumval3lem2  19026  selvval  20331  kgencn2  22165  upxp  22231  uptx  22233  txcn  22234  xkococnlem  22267  xkococn  22268  cnmptk1  22289  cnmptkk  22291  xkofvcn  22292  imasdsf1olem  22983  pi1cof  23663  pi1coval  23664  elovolmr  24077  ovoliunlem3  24105  ismbf1  24225  motplusg  26328  hocsubdir  29562  hoddi  29767  lnopco0i  29781  opsqrlem1  29917  pjsdi2i  29934  pjin2i  29970  pjclem1  29972  symgfcoeu  30726  eulerpartgbij  31630  cvmliftmo  32531  cvmliftlem14  32544  cvmliftiota  32548  cvmlift2lem13  32562  cvmlift2  32563  cvmliftphtlem  32564  cvmlift3lem2  32567  cvmlift3lem6  32571  cvmlift3lem7  32572  cvmlift3lem9  32574  cvmlift3  32575  msubco  32778  ftc1anclem8  34989  upixp  35019  coideq  35522  xrneq1  35644  xrneq2  35647  trlcoat  37874  trljco  37891  tgrpov  37899  tendovalco  37916  erngmul  37957  erngmul-rN  37965  dvamulr  38163  dvavadd  38166  dvhmulr  38237  dihjatcclem4  38572  mendmulr  39808  hoiprodcl2  42857  ovnlecvr  42860  ovncvrrp  42866  ovnsubaddlem2  42873  ovncvr2  42913  opnvonmbllem1  42934  opnvonmbl  42936  ovolval4lem2  42952  ovolval5lem2  42955  ovolval5lem3  42956  ovolval5  42957  ovnovollem2  42959  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  ringcinvALTV  44347