Theorem coeq2 5800

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ⊆ wss 3883   ∘ ccom 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5073  df-opab 5135  df-co 5627

This theorem is referenced by:  coeq2i  5802  coeq2d  5804  coi2  6215  f1eqcocnv  7245  ereq1  8641  dfttrcl2  9636  seqf1olem2  13995  seqf1o  13996  relexpsucnnr  14978  isps  18525  pwsco2mhm  18792  gsumwmhm  18804  frmdgsum  18821  frmdup1  18823  frmdup2  18824  efmndov  18840  symggrplem  18843  smndex1mndlem  18871  smndex1mnd  18872  pmtr3ncom  19441  psgnunilem1  19459  frgpuplem  19738  frgpupf  19739  frgpupval  19740  gsumval3eu  19870  gsumval3lem2  19872  rngcinv  20609  ringcinv  20643  selvval  22096  rhmmpl  22366  rhmply1vr1  22370  rhmply1vsca  22371  kgencn2  23540  upxp  23606  uptx  23608  txcn  23609  xkococnlem  23642  xkococn  23643  cnmptk1  23664  cnmptkk  23666  xkofvcn  23667  imasdsf1olem  24356  pi1cof  25044  pi1coval  25045  elovolmr  25461  ovoliunlem3  25489  ismbf1  25609  motplusg  28628  hocsubdir  31874  hoddi  32079  lnopco0i  32093  opsqrlem1  32229  pjsdi2i  32246  pjin2i  32282  pjclem1  32284  symgfcoeu  33163  1arithidomlem1  33618  1arithidom  33620  mplvrpmfgalem  33728  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  splysubrg  33744  issply  33745  eulerpartgbij  34556  cvmliftmo  35512  cvmliftlem14  35525  cvmliftiota  35529  cvmlift2lem13  35543  cvmlift2  35544  cvmliftphtlem  35545  cvmlift3lem2  35548  cvmlift3lem6  35552  cvmlift3lem7  35553  cvmlift3lem9  35555  cvmlift3  35556  msubco  35759  ftc1anclem8  38067  upixp  38096  coideq  38615  xrneq1  38763  xrneq2  38766  shiftstableeq2  38850  trlcoat  41215  trljco  41232  tgrpov  41240  tendovalco  41257  erngmul  41298  erngmul-rN  41306  dvamulr  41504  dvavadd  41507  dvhmulr  41578  dihjatcclem4  41913  rhmpsr  43033  mendmulr  43629  hoiprodcl2  46998  ovnlecvr  47001  ovncvrrp  47007  ovnsubaddlem2  47014  ovncvr2  47054  opnvonmbllem1  47075  opnvonmbl  47077  ovolval4lem2  47093  ovolval5lem2  47096  ovolval5lem3  47097  ovolval5  47098  ovnovollem2  47100  rngcinvALTV  48767  ringcinvALTV  48801  itcoval1  49154  itcoval2  49155  itcoval3  49156  itcovalsucov  49159