Theorem coeq2 5822

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3914   ∘ ccom 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-br 5108  df-opab 5170  df-co 5647

This theorem is referenced by:  coeq2i  5824  coeq2d  5826  coi2  6236  f1eqcocnv  7276  ereq1  8678  dfttrcl2  9677  seqf1olem2  14007  seqf1o  14008  relexpsucnnr  14991  isps  18527  pwsco2mhm  18760  gsumwmhm  18772  frmdgsum  18789  frmdup1  18791  frmdup2  18792  efmndov  18808  symggrplem  18811  smndex1mndlem  18836  smndex1mnd  18837  pmtr3ncom  19405  psgnunilem1  19423  frgpuplem  19702  frgpupf  19703  frgpupval  19704  gsumval3eu  19834  gsumval3lem2  19836  rngcinv  20546  ringcinv  20580  selvval  22022  rhmmpl  22270  rhmply1vr1  22274  rhmply1vsca  22275  kgencn2  23444  upxp  23510  uptx  23512  txcn  23513  xkococnlem  23546  xkococn  23547  cnmptk1  23568  cnmptkk  23570  xkofvcn  23571  imasdsf1olem  24261  pi1cof  24959  pi1coval  24960  elovolmr  25377  ovoliunlem3  25405  ismbf1  25525  motplusg  28469  hocsubdir  31714  hoddi  31919  lnopco0i  31933  opsqrlem1  32069  pjsdi2i  32086  pjin2i  32122  pjclem1  32124  symgfcoeu  33039  1arithidomlem1  33506  1arithidom  33508  eulerpartgbij  34363  cvmliftmo  35271  cvmliftlem14  35284  cvmliftiota  35288  cvmlift2lem13  35302  cvmlift2  35303  cvmliftphtlem  35304  cvmlift3lem2  35307  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  cvmlift3  35315  msubco  35518  ftc1anclem8  37694  upixp  37723  coideq  38235  xrneq1  38363  xrneq2  38366  trlcoat  40717  trljco  40734  tgrpov  40742  tendovalco  40759  erngmul  40800  erngmul-rN  40808  dvamulr  41006  dvavadd  41009  dvhmulr  41080  dihjatcclem4  41415  rhmpsr  42540  mendmulr  43173  hoiprodcl2  46553  ovnlecvr  46556  ovncvrrp  46562  ovnsubaddlem2  46569  ovncvr2  46609  opnvonmbllem1  46630  opnvonmbl  46632  ovolval4lem2  46648  ovolval5lem2  46651  ovolval5lem3  46652  ovolval5  46653  ovnovollem2  46655  rngcinvALTV  48264  ringcinvALTV  48298  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsucov  48657