Theorem coeq2 5845

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ⊆ wss 3913   ∘ ccom 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5114  df-opab 5178  df-co 5671

This theorem is referenced by:  coeq2i  5847  coeq2d  5849  coi2  6266  f1eqcocnv  7300  ereq1  8702  dfttrcl2  9693  seqf1olem2  14078  seqf1o  14079  relexpsucnnr  15062  isps  18624  pwsco2mhm  18892  gsumwmhm  18904  frmdgsum  18921  frmdup1  18923  frmdup2  18924  efmndov  18940  symggrplem  18943  smndex1mndlem  18971  smndex1mnd  18972  pmtr3ncom  19545  psgnunilem1  19563  frgpuplem  19842  frgpupf  19843  frgpupval  19844  gsumval3eu  19974  gsumval3lem2  19976  rngcinv  20722  ringcinv  20756  selvval  22240  rhmmpl  22509  rhmply1vr1  22513  rhmply1vsca  22514  kgencn2  23683  upxp  23749  uptx  23751  txcn  23752  xkococnlem  23785  xkococn  23786  cnmptk1  23807  cnmptkk  23809  xkofvcn  23810  imasdsf1olem  24499  pi1cof  25187  pi1coval  25188  elovolmr  25604  ovoliunlem3  25632  ismbf1  25752  motplusg  28777  hocsubdir  32078  hoddi  32283  lnopco0i  32297  opsqrlem1  32433  pjsdi2i  32450  pjin2i  32486  pjclem1  32488  symgfcoeu  33343  1arithidomlem1  33770  1arithidom  33772  mplvrpmfgalem  33879  mplvrpmga  33880  mplvrpmmhm  33881  mplvrpmrhm  33882  splysubrg  33895  issply  33896  eulerpartgbij  34707  cvmliftmo  35675  cvmliftlem14  35688  cvmliftiota  35692  cvmlift2lem13  35706  cvmlift2  35707  cvmliftphtlem  35708  cvmlift3lem2  35711  cvmlift3lem6  35715  cvmlift3lem7  35716  cvmlift3lem9  35718  cvmlift3  35719  msubco  35922  ftc1anclem8  38239  upixp  38268  coideq  38787  xrneq1  38935  xrneq2  38938  shiftstableeq2  39022  trlcoat  41387  trljco  41404  tgrpov  41412  tendovalco  41429  erngmul  41470  erngmul-rN  41478  dvamulr  41676  dvavadd  41679  dvhmulr  41750  dihjatcclem4  42085  rhmpsr  43207  mendmulr  43803  hoiprodcl2  47161  ovnlecvr  47164  ovncvrrp  47170  ovnsubaddlem2  47177  ovncvr2  47217  opnvonmbllem1  47238  opnvonmbl  47240  ovolval4lem2  47256  ovolval5lem2  47259  ovolval5lem3  47260  ovolval5  47261  ovnovollem2  47263  rngcinvALTV  48930  ringcinvALTV  48964  itcoval1  49328  itcoval2  49329  itcoval3  49330  itcovalsucov  49333