Theorem coeq2 5846

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3906   ∘ ccom 5667

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-co 5672

This theorem is used by:  coeq2i  5848  coeq2d  5850  coi2  6267  f1eqcocnv  7308  ereq1  8708  dfttrcl2  9700  seqf1olem2  14098  seqf1o  14099  relexpsucnnr  15088  isps  18648  pwsco2mhm  18931  gsumwmhm  18943  frmdgsum  18960  frmdup1  18962  frmdup2  18963  efmndov  18979  symggrplem  18982  smndex1mndlem  19010  smndex1mnd  19011  pmtr3ncom  19591  psgnunilem1  19609  frgpuplem  19888  frgpupf  19889  frgpupval  19890  gsumval3eu  20020  gsumval3lem2  20022  rngcinv  20788  ringcinv  20822  selvval  22323  rhmmpl  22592  rhmply1vr1  22596  rhmply1vsca  22597  kgencn2  23767  upxp  23833  uptx  23835  txcn  23836  xkococnlem  23869  xkococn  23870  cnmptk1  23891  cnmptkk  23893  xkofvcn  23894  imasdsf1olem  24583  pi1cof  25271  pi1coval  25272  elovolmr  25688  ovoliunlem3  25716  ismbf1  25836  motplusg  28864  hocsubdir  32210  hoddi  32415  lnopco0i  32429  opsqrlem1  32565  pjsdi2i  32582  pjin2i  32618  pjclem1  32620  symgfcoeu  33468  1arithidomlem1  33891  1arithidom  33893  mplvrpmfgalem  34000  mplvrpmga  34001  mplvrpmmhm  34002  mplvrpmrhm  34003  splysubrg  34016  issply  34017  eulerpartgbij  34829  cvmliftmo  35815  cvmliftlem14  35828  cvmliftiota  35832  cvmlift2lem13  35846  cvmlift2  35847  cvmliftphtlem  35848  cvmlift3lem2  35851  cvmlift3lem6  35855  cvmlift3lem7  35856  cvmlift3lem9  35858  cvmlift3  35859  msubco  36062  ftc1anclem8  38410  upixp  38440  coideq  38957  xrneq1  39105  xrneq2  39108  shiftstableeq2  39192  trlcoat  41557  trljco  41574  tgrpov  41582  tendovalco  41599  erngmul  41640  erngmul-rN  41648  dvamulr  41846  dvavadd  41849  dvhmulr  41920  dihjatcclem4  42255  rhmpsr  43375  mendmulr  43971  hoiprodcl2  47329  ovnlecvr  47332  ovncvrrp  47338  ovnsubaddlem2  47345  ovncvr2  47385  opnvonmbllem1  47406  opnvonmbl  47408  ovolval4lem2  47424  ovolval5lem2  47427  ovolval5lem3  47428  ovolval5  47429  ovnovollem2  47431  rngcinvALTV  49100  ringcinvALTV  49134  itcoval1  49502  itcoval2  49503  itcoval3  49504  itcovalsucov  49507