Theorem coeq2 5872

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3963   ∘ ccom 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-br 5149  df-opab 5211  df-co 5698

This theorem is referenced by:  coeq2i  5874  coeq2d  5876  coi2  6285  f1eqcocnv  7321  ereq1  8751  dfttrcl2  9762  seqf1olem2  14080  seqf1o  14081  relexpsucnnr  15061  isps  18626  pwsco2mhm  18859  gsumwmhm  18871  frmdgsum  18888  frmdup1  18890  frmdup2  18891  efmndov  18907  symggrplem  18910  smndex1mndlem  18935  smndex1mnd  18936  pmtr3ncom  19508  psgnunilem1  19526  frgpuplem  19805  frgpupf  19806  frgpupval  19807  gsumval3eu  19937  gsumval3lem2  19939  rngcinv  20654  ringcinv  20688  selvval  22157  rhmmpl  22403  rhmply1vr1  22407  rhmply1vsca  22408  kgencn2  23581  upxp  23647  uptx  23649  txcn  23650  xkococnlem  23683  xkococn  23684  cnmptk1  23705  cnmptkk  23707  xkofvcn  23708  imasdsf1olem  24399  pi1cof  25106  pi1coval  25107  elovolmr  25525  ovoliunlem3  25553  ismbf1  25673  motplusg  28565  hocsubdir  31814  hoddi  32019  lnopco0i  32033  opsqrlem1  32169  pjsdi2i  32186  pjin2i  32222  pjclem1  32224  symgfcoeu  33085  1arithidomlem1  33543  1arithidom  33545  eulerpartgbij  34354  cvmliftmo  35269  cvmliftlem14  35282  cvmliftiota  35286  cvmlift2lem13  35300  cvmlift2  35301  cvmliftphtlem  35302  cvmlift3lem2  35305  cvmlift3lem6  35309  cvmlift3lem7  35310  cvmlift3lem9  35312  cvmlift3  35313  msubco  35516  ftc1anclem8  37687  upixp  37716  coideq  38228  xrneq1  38359  xrneq2  38362  trlcoat  40706  trljco  40723  tgrpov  40731  tendovalco  40748  erngmul  40789  erngmul-rN  40797  dvamulr  40995  dvavadd  40998  dvhmulr  41069  dihjatcclem4  41404  rhmpsr  42539  mendmulr  43173  hoiprodcl2  46511  ovnlecvr  46514  ovncvrrp  46520  ovnsubaddlem2  46527  ovncvr2  46567  opnvonmbllem1  46588  opnvonmbl  46590  ovolval4lem2  46606  ovolval5lem2  46609  ovolval5lem3  46610  ovolval5  46611  ovnovollem2  46613  rngcinvALTV  48120  ringcinvALTV  48154  itcoval1  48513  itcoval2  48514  itcoval3  48515  itcovalsucov  48518