Theorem coeq2 5844

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ⊆ wss 3905   ∘ ccom 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-co 5670

This theorem is referenced by:  coeq2i  5846  coeq2d  5848  coi2  6265  f1eqcocnv  7299  ereq1  8698  dfttrcl2  9689  seqf1olem2  14074  seqf1o  14075  relexpsucnnr  15058  isps  18619  pwsco2mhm  18887  gsumwmhm  18899  frmdgsum  18916  frmdup1  18918  frmdup2  18919  efmndov  18935  symggrplem  18938  smndex1mndlem  18966  smndex1mnd  18967  pmtr3ncom  19540  psgnunilem1  19558  frgpuplem  19837  frgpupf  19838  frgpupval  19839  gsumval3eu  19969  gsumval3lem2  19971  rngcinv  20736  ringcinv  20770  selvval  22271  rhmmpl  22540  rhmply1vr1  22544  rhmply1vsca  22545  kgencn2  23714  upxp  23780  uptx  23782  txcn  23783  xkococnlem  23816  xkococn  23817  cnmptk1  23838  cnmptkk  23840  xkofvcn  23841  imasdsf1olem  24530  pi1cof  25218  pi1coval  25219  elovolmr  25635  ovoliunlem3  25663  ismbf1  25783  motplusg  28811  hocsubdir  32137  hoddi  32342  lnopco0i  32356  opsqrlem1  32492  pjsdi2i  32509  pjin2i  32545  pjclem1  32547  symgfcoeu  33402  1arithidomlem1  33825  1arithidom  33827  mplvrpmfgalem  33934  mplvrpmga  33935  mplvrpmmhm  33936  mplvrpmrhm  33937  splysubrg  33950  issply  33951  eulerpartgbij  34762  cvmliftmo  35776  cvmliftlem14  35789  cvmliftiota  35793  cvmlift2lem13  35807  cvmlift2  35808  cvmliftphtlem  35809  cvmlift3lem2  35812  cvmlift3lem6  35816  cvmlift3lem7  35817  cvmlift3lem9  35819  cvmlift3  35820  msubco  36023  ftc1anclem8  38371  upixp  38400  coideq  38917  xrneq1  39065  xrneq2  39068  shiftstableeq2  39152  trlcoat  41517  trljco  41534  tgrpov  41542  tendovalco  41559  erngmul  41600  erngmul-rN  41608  dvamulr  41806  dvavadd  41809  dvhmulr  41880  dihjatcclem4  42215  rhmpsr  43335  mendmulr  43931  hoiprodcl2  47289  ovnlecvr  47292  ovncvrrp  47298  ovnsubaddlem2  47305  ovncvr2  47345  opnvonmbllem1  47366  opnvonmbl  47368  ovolval4lem2  47384  ovolval5lem2  47387  ovolval5lem3  47388  ovolval5  47389  ovnovollem2  47391  rngcinvALTV  49061  ringcinvALTV  49095  itcoval1  49463  itcoval2  49464  itcoval3  49465  itcovalsucov  49468