Theorem coeq2 5573

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ⊆ wss 3823   ∘ ccom 5405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-in 3830  df-ss 3837  df-br 4924  df-opab 4986  df-co 5410

This theorem is referenced by:  coeq2i  5575  coeq2d  5577  coi2  5949  relcnvtr  5952  f1eqcocnv  6876  ereq1  8090  seqf1olem2  13219  seqf1o  13220  relexpsucnnr  14239  isps  17664  pwsco2mhm  17833  gsumwmhm  17845  frmdgsum  17862  frmdup1  17864  frmdup2  17865  symgov  18273  pmtr3ncom  18358  psgnunilem1  18376  frgpuplem  18652  frgpupf  18653  frgpupval  18654  gsumval3eu  18772  gsumval3lem2  18774  kgencn2  21863  upxp  21929  uptx  21931  txcn  21932  xkococnlem  21965  xkococn  21966  cnmptk1  21987  cnmptkk  21989  xkofvcn  21990  imasdsf1olem  22680  pi1cof  23360  pi1coval  23361  elovolmr  23774  ovoliunlem3  23802  ismbf1  23922  motplusg  26024  hocsubdir  29337  hoddi  29542  lnopco0i  29556  opsqrlem1  29692  pjsdi2i  29709  pjin2i  29745  pjclem1  29747  symgfcoeu  30687  eulerpartgbij  31275  cvmliftmo  32116  cvmliftlem14  32129  cvmliftiota  32133  cvmlift2lem13  32147  cvmlift2  32148  cvmliftphtlem  32149  cvmlift3lem2  32152  cvmlift3lem6  32156  cvmlift3lem7  32157  cvmlift3lem9  32159  cvmlift3  32160  msubco  32298  ftc1anclem8  34415  upixp  34446  coideq  34951  xrneq1  35074  xrneq2  35077  trlcoat  37304  trljco  37321  tgrpov  37329  tendovalco  37346  erngmul  37387  erngmul-rN  37395  dvamulr  37593  dvavadd  37596  dvhmulr  37667  dihjatcclem4  38002  mendmulr  39184  hoiprodcl2  42268  ovnlecvr  42271  ovncvrrp  42277  ovnsubaddlem2  42284  ovncvr2  42324  opnvonmbllem1  42345  opnvonmbl  42347  ovolval4lem2  42363  ovolval5lem2  42366  ovolval5lem3  42367  ovolval5  42368  ovnovollem2  42370  rngcinv  43616  rngcinvALTV  43628  ringcinv  43667  ringcinvALTV  43691