Theorem coeq2 5807

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3901   ∘ ccom 5628

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-br 5099  df-opab 5161  df-co 5633

This theorem is referenced by:  coeq2i  5809  coeq2d  5811  coi2  6222  f1eqcocnv  7247  ereq1  8642  dfttrcl2  9633  seqf1olem2  13965  seqf1o  13966  relexpsucnnr  14948  isps  18491  pwsco2mhm  18758  gsumwmhm  18770  frmdgsum  18787  frmdup1  18789  frmdup2  18790  efmndov  18806  symggrplem  18809  smndex1mndlem  18834  smndex1mnd  18835  pmtr3ncom  19404  psgnunilem1  19422  frgpuplem  19701  frgpupf  19702  frgpupval  19703  gsumval3eu  19833  gsumval3lem2  19835  rngcinv  20570  ringcinv  20604  selvval  22078  rhmmpl  22327  rhmply1vr1  22331  rhmply1vsca  22332  kgencn2  23501  upxp  23567  uptx  23569  txcn  23570  xkococnlem  23603  xkococn  23604  cnmptk1  23625  cnmptkk  23627  xkofvcn  23628  imasdsf1olem  24317  pi1cof  25015  pi1coval  25016  elovolmr  25433  ovoliunlem3  25461  ismbf1  25581  motplusg  28614  hocsubdir  31860  hoddi  32065  lnopco0i  32079  opsqrlem1  32215  pjsdi2i  32232  pjin2i  32268  pjclem1  32270  symgfcoeu  33164  1arithidomlem1  33616  1arithidom  33618  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  splysubrg  33718  issply  33719  eulerpartgbij  34529  cvmliftmo  35478  cvmliftlem14  35491  cvmliftiota  35495  cvmlift2lem13  35509  cvmlift2  35510  cvmliftphtlem  35511  cvmlift3lem2  35514  cvmlift3lem6  35518  cvmlift3lem7  35519  cvmlift3lem9  35521  cvmlift3  35522  msubco  35725  ftc1anclem8  37901  upixp  37930  coideq  38444  xrneq1  38591  xrneq2  38594  trlcoat  40993  trljco  41010  tgrpov  41018  tendovalco  41035  erngmul  41076  erngmul-rN  41084  dvamulr  41282  dvavadd  41285  dvhmulr  41356  dihjatcclem4  41691  rhmpsr  42815  mendmulr  43436  hoiprodcl2  46809  ovnlecvr  46812  ovncvrrp  46818  ovnsubaddlem2  46825  ovncvr2  46865  opnvonmbllem1  46886  opnvonmbl  46888  ovolval4lem2  46904  ovolval5lem2  46907  ovolval5lem3  46908  ovolval5  46909  ovnovollem2  46911  rngcinvALTV  48532  ringcinvALTV  48566  itcoval1  48919  itcoval2  48920  itcoval3  48921  itcovalsucov  48924