Theorem coeq2 5813

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3889   ∘ ccom 5635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-co 5640

This theorem is referenced by:  coeq2i  5815  coeq2d  5817  coi2  6228  f1eqcocnv  7256  ereq1  8651  dfttrcl2  9645  seqf1olem2  14004  seqf1o  14005  relexpsucnnr  14987  isps  18534  pwsco2mhm  18801  gsumwmhm  18813  frmdgsum  18830  frmdup1  18832  frmdup2  18833  efmndov  18849  symggrplem  18852  smndex1mndlem  18880  smndex1mnd  18881  pmtr3ncom  19450  psgnunilem1  19468  frgpuplem  19747  frgpupf  19748  frgpupval  19749  gsumval3eu  19879  gsumval3lem2  19881  rngcinv  20614  ringcinv  20648  selvval  22101  rhmmpl  22348  rhmply1vr1  22352  rhmply1vsca  22353  kgencn2  23522  upxp  23588  uptx  23590  txcn  23591  xkococnlem  23624  xkococn  23625  cnmptk1  23646  cnmptkk  23648  xkofvcn  23649  imasdsf1olem  24338  pi1cof  25026  pi1coval  25027  elovolmr  25443  ovoliunlem3  25471  ismbf1  25591  motplusg  28610  hocsubdir  31856  hoddi  32061  lnopco0i  32075  opsqrlem1  32211  pjsdi2i  32228  pjin2i  32264  pjclem1  32266  symgfcoeu  33143  1arithidomlem1  33595  1arithidom  33597  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  splysubrg  33704  issply  33705  eulerpartgbij  34516  cvmliftmo  35466  cvmliftlem14  35479  cvmliftiota  35483  cvmlift2lem13  35497  cvmlift2  35498  cvmliftphtlem  35499  cvmlift3lem2  35502  cvmlift3lem6  35506  cvmlift3lem7  35507  cvmlift3lem9  35509  cvmlift3  35510  msubco  35713  ftc1anclem8  38021  upixp  38050  coideq  38569  xrneq1  38717  xrneq2  38720  shiftstableeq2  38804  trlcoat  41169  trljco  41186  tgrpov  41194  tendovalco  41211  erngmul  41252  erngmul-rN  41260  dvamulr  41458  dvavadd  41461  dvhmulr  41532  dihjatcclem4  41867  rhmpsr  42995  mendmulr  43612  hoiprodcl2  46983  ovnlecvr  46986  ovncvrrp  46992  ovnsubaddlem2  46999  ovncvr2  47039  opnvonmbllem1  47060  opnvonmbl  47062  ovolval4lem2  47078  ovolval5lem2  47081  ovolval5lem3  47082  ovolval5  47083  ovnovollem2  47085  rngcinvALTV  48752  ringcinvALTV  48786  itcoval1  49139  itcoval2  49140  itcoval3  49141  itcovalsucov  49144