Theorem coeq2 5202

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ⊆ wss 3540   ∘ ccom 5042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-co 5047

This theorem is referenced by:  coeq2i  5204  coeq2d  5206  coi2  5569  relcnvtr  5572  f1eqcocnv  6456  ereq1  7636  seqf1olem2  12703  seqf1o  12704  relexpsucnnr  13613  isps  17025  pwsco2mhm  17194  gsumwmhm  17205  frmdgsum  17222  frmdup1  17224  frmdup2  17225  symgov  17633  pmtr3ncom  17718  psgnunilem1  17736  frgpuplem  18008  frgpupf  18009  frgpupval  18010  gsumval3eu  18128  gsumval3lem2  18130  kgencn2  21170  upxp  21236  uptx  21238  txcn  21239  xkococnlem  21272  xkococn  21273  cnmptk1  21294  cnmptkk  21296  xkofvcn  21297  imasdsf1olem  21988  pi1cof  22667  pi1coval  22668  elovolmr  23051  ovoliunlem3  23079  ismbf1  23199  motplusg  25237  hocsubdir  28028  hoddi  28233  lnopco0i  28247  opsqrlem1  28383  pjsdi2i  28400  pjin2i  28436  pjclem1  28438  symgfcoeu  29176  eulerpartgbij  29761  cvmliftmo  30520  cvmliftlem14  30533  cvmliftiota  30537  cvmlift2lem13  30551  cvmlift2  30552  cvmliftphtlem  30553  cvmlift3lem2  30556  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem9  30563  cvmlift3  30564  msubco  30682  ftc1anclem8  32662  upixp  32694  trlcoat  35029  trljco  35046  tgrpov  35054  tendovalco  35071  erngmul  35112  erngmul-rN  35120  dvamulr  35318  dvavadd  35321  dvhmulr  35393  dihjatcclem4  35728  mendmulr  36777  hoiprodcl2  39445  ovnlecvr  39448  ovncvrrp  39454  ovnsubaddlem2  39461  ovncvr2  39501  opnvonmbllem1  39522  opnvonmbl  39524  ovolval4lem2  39540  ovolval5lem2  39543  ovolval5lem3  39544  ovolval5  39545  ovnovollem2  39547  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848