Theorem coeq2 5830

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ⊆ wss 3904   ∘ ccom 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5101  df-opab 5163  df-co 5656

This theorem is referenced by:  coeq2i  5832  coeq2d  5834  coi2  6251  f1eqcocnv  7285  ereq1  8686  dfttrcl2  9679  seqf1olem2  14055  seqf1o  14056  relexpsucnnr  15038  isps  18600  pwsco2mhm  18867  gsumwmhm  18879  frmdgsum  18896  frmdup1  18898  frmdup2  18899  efmndov  18915  symggrplem  18918  smndex1mndlem  18946  smndex1mnd  18947  pmtr3ncom  19515  psgnunilem1  19533  frgpuplem  19812  frgpupf  19813  frgpupval  19814  gsumval3eu  19944  gsumval3lem2  19946  rngcinv  20687  ringcinv  20721  selvval  22173  rhmmpl  22443  rhmply1vr1  22447  rhmply1vsca  22448  kgencn2  23617  upxp  23683  uptx  23685  txcn  23686  xkococnlem  23719  xkococn  23720  cnmptk1  23741  cnmptkk  23743  xkofvcn  23744  imasdsf1olem  24433  pi1cof  25121  pi1coval  25122  elovolmr  25538  ovoliunlem3  25566  ismbf1  25686  motplusg  28711  hocsubdir  31988  hoddi  32193  lnopco0i  32207  opsqrlem1  32343  pjsdi2i  32360  pjin2i  32396  pjclem1  32398  symgfcoeu  33262  1arithidomlem1  33731  1arithidom  33733  mplvrpmfgalem  33841  mplvrpmga  33842  mplvrpmmhm  33843  mplvrpmrhm  33844  splysubrg  33857  issply  33858  eulerpartgbij  34669  cvmliftmo  35634  cvmliftlem14  35647  cvmliftiota  35651  cvmlift2lem13  35665  cvmlift2  35666  cvmliftphtlem  35667  cvmlift3lem2  35670  cvmlift3lem6  35674  cvmlift3lem7  35675  cvmlift3lem9  35677  cvmlift3  35678  msubco  35881  ftc1anclem8  38199  upixp  38228  coideq  38747  xrneq1  38895  xrneq2  38898  shiftstableeq2  38982  trlcoat  41347  trljco  41364  tgrpov  41372  tendovalco  41389  erngmul  41430  erngmul-rN  41438  dvamulr  41636  dvavadd  41639  dvhmulr  41710  dihjatcclem4  42045  rhmpsr  43165  mendmulr  43761  hoiprodcl2  47129  ovnlecvr  47132  ovncvrrp  47138  ovnsubaddlem2  47145  ovncvr2  47185  opnvonmbllem1  47206  opnvonmbl  47208  ovolval4lem2  47224  ovolval5lem2  47227  ovolval5lem3  47228  ovolval5  47229  ovnovollem2  47231  rngcinvALTV  48898  ringcinvALTV  48932  itcoval1  49285  itcoval2  49286  itcoval3  49287  itcovalsucov  49290