Theorem coeq2 5840

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ⊆ wss 3899   ∘ ccom 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3900  df-br 5106  df-opab 5170  df-co 5663

This theorem is used by:  coeq2i  5842  coeq2d  5844  coi2  6271  f1eqcocnv  7316  ereq1  8736  dfttrcl2  9735  seqf1olem2  14195  seqf1o  14196  relexpsucnnr  15190  isps  18754  pwsco2mhm  19041  gsumwmhm  19053  frmdgsum  19070  frmdup1  19072  frmdup2  19073  efmndov  19089  symggrplem  19092  smndex1mndlem  19120  smndex1mnd  19121  pmtr3ncom  19701  psgnunilem1  19719  frgpuplem  19998  frgpupf  19999  frgpupval  20000  gsumval3eu  20130  gsumval3lem2  20132  rngcinv  20901  ringcinv  20935  selvval  22441  rhmmpl  22710  rhmply1vr1  22714  rhmply1vsca  22715  kgencn2  23888  upxp  23954  uptx  23956  txcn  23957  xkococnlem  23990  xkococn  23991  cnmptk1  24012  cnmptkk  24014  xkofvcn  24015  imasdsf1olem  24704  pi1cof  25392  pi1coval  25393  elovolmr  25809  ovoliunlem3  25837  ismbf1  25957  motplusg  29017  hocsubdir  32399  hoddi  32604  lnopco0i  32618  opsqrlem1  32754  pjsdi2i  32771  pjin2i  32807  pjclem1  32809  symgfcoeu  33696  1arithidomlem1  34120  1arithidom  34122  mplvrpmfgalem  34229  mplvrpmga  34230  mplvrpmmhm  34231  mplvrpmrhm  34232  splysubrg  34245  issply  34246  eulerpartgbij  35057  cvmliftmo  36170  cvmliftlem14  36183  cvmliftiota  36187  cvmlift2lem13  36201  cvmlift2  36202  cvmliftphtlem  36203  cvmlift3lem2  36206  cvmlift3lem6  36210  cvmlift3lem7  36211  cvmlift3lem9  36213  cvmlift3  36214  msubco  36417  ftc1anclem8  38758  upixp  38803  coideq  39320  xrneq1  39468  xrneq2  39471  shiftstableeq2  39555  trlcoat  41920  trljco  41937  tgrpov  41945  tendovalco  41962  erngmul  42003  erngmul-rN  42011  dvamulr  42209  dvavadd  42212  dvhmulr  42283  dihjatcclem4  42618  rhmpsr  43751  mendmulr  44326  hoiprodcl2  47704  ovnlecvr  47707  ovncvrrp  47713  ovnsubaddlem2  47720  ovncvr2  47760  opnvonmbllem1  47781  opnvonmbl  47783  ovolval4lem2  47799  ovolval5lem2  47802  ovolval5lem3  47803  ovolval5  47804  ovnovollem2  47806  rngcinvALTV  49512  ringcinvALTV  49546  itcoval1  49914  itcoval2  49915  itcoval3  49916  itcovalsucov  49919