Theorem coeq1 5804

Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)

Assertion

Ref	Expression
coeq1	⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Proof of Theorem coeq1

Step	Hyp	Ref	Expression
1		coss1 5802	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
2		coss1 5802	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)))
4		eqss 3947	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3947	. 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3899   ∘ ccom 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-br 5097  df-opab 5159  df-co 5631

This theorem is referenced by:  coeq1i  5806  coeq1d  5808  coi2  6220  funcoeqres  6803  wrecseq123  8253  ereq1  8640  domssex2  9063  wemapwe  9604  dfttrcl2  9631  updjud  9844  seqf1olem2  13963  seqf1o  13964  relexpsucnnl  14951  isps  18489  pwsco1mhm  18755  frmdup3  18790  efmndov  18804  symggrplem  18807  smndex1mndlem  18832  smndex1mnd  18833  pmtr3ncom  19402  psgnunilem1  19420  frgpup3  19705  gsumval3  19834  rngcinv  20568  ringcinv  20602  frgpcyg  21526  frlmup4  21754  evlseu  22036  evlsval2  22040  evlsval3  22042  selvval  22076  evls1val  22262  evls1sca  22265  evl1val  22271  mpfpf1  22293  pf1mpf  22294  pf1ind  22297  xkococnlem  23601  xkococn  23602  cnmpt1k  23624  cnmptkk  23625  xkofvcn  23626  qtopeu  23658  qtophmeo  23759  utop2nei  24192  cncombf  25613  dgrcolem2  26234  dgrco  26235  motplusg  28563  hocsubdir  31809  hoddi  32014  opsqrlem1  32164  1arithidom  33567  mplvrpmga  33659  mplvrpmrhm  33661  issply  33668  smatfval  33901  msubco  35674  coideq  38383  trljco  40939  tgrpov  40947  tendovalco  40964  erngmul  41005  erngmul-rN  41013  cdlemksv  41043  cdlemkuu  41094  cdlemk41  41119  cdleml5N  41179  cdleml9  41183  dvamulr  41211  dvavadd  41214  dvhmulr  41285  dvhvscacbv  41297  dvhvscaval  41298  dih1dimatlem0  41527  dihjatcclem4  41620  diophrw  42943  eldioph2  42946  diophren  42997  mendmulr  43368  fundcmpsurinjpreimafv  47596  rngcinvALTV  48464  ringcinvALTV  48498  itcoval  48849  setc1ocofval  49681