Theorem coeq2 5732

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ⊆ wss 3939   ∘ ccom 5562

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-in 3946  df-ss 3955  df-br 5070  df-opab 5132  df-co 5567

This theorem is referenced by:  coeq2i  5734  coeq2d  5736  coi2  6119  f1eqcocnv  7060  ereq1  8299  seqf1olem2  13413  seqf1o  13414  relexpsucnnr  14387  isps  17815  pwsco2mhm  18000  gsumwmhm  18013  frmdgsum  18030  frmdup1  18032  frmdup2  18033  efmndov  18049  symggrplem  18052  smndex1mndlem  18077  smndex1mnd  18078  pmtr3ncom  18606  psgnunilem1  18624  frgpuplem  18901  frgpupf  18902  frgpupval  18903  gsumval3eu  19027  gsumval3lem2  19029  selvval  20334  kgencn2  22168  upxp  22234  uptx  22236  txcn  22237  xkococnlem  22270  xkococn  22271  cnmptk1  22292  cnmptkk  22294  xkofvcn  22295  imasdsf1olem  22986  pi1cof  23666  pi1coval  23667  elovolmr  24080  ovoliunlem3  24108  ismbf1  24228  motplusg  26331  hocsubdir  29565  hoddi  29770  lnopco0i  29784  opsqrlem1  29920  pjsdi2i  29937  pjin2i  29973  pjclem1  29975  symgfcoeu  30730  eulerpartgbij  31634  cvmliftmo  32535  cvmliftlem14  32548  cvmliftiota  32552  cvmlift2lem13  32566  cvmlift2  32567  cvmliftphtlem  32568  cvmlift3lem2  32571  cvmlift3lem6  32575  cvmlift3lem7  32576  cvmlift3lem9  32578  cvmlift3  32579  msubco  32782  ftc1anclem8  34978  upixp  35008  coideq  35511  xrneq1  35633  xrneq2  35636  trlcoat  37863  trljco  37880  tgrpov  37888  tendovalco  37905  erngmul  37946  erngmul-rN  37954  dvamulr  38152  dvavadd  38155  dvhmulr  38226  dihjatcclem4  38561  mendmulr  39794  hoiprodcl2  42844  ovnlecvr  42847  ovncvrrp  42853  ovnsubaddlem2  42860  ovncvr2  42900  opnvonmbllem1  42921  opnvonmbl  42923  ovolval4lem2  42939  ovolval5lem2  42942  ovolval5lem3  42943  ovolval5  42944  ovnovollem2  42946  rngcinv  44259  rngcinvALTV  44271  ringcinv  44310  ringcinvALTV  44334