Theorem coeq1 5201

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 5199	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
2		coss1 5199	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶))
3	1, 2	anim12i 588	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)))
4		eqss 3583	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3583	. 2 ⊢ ((𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) ↔ ((𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶) ∧ (𝐵 ∘ 𝐶) ⊆ (𝐴 ∘ 𝐶)))
6	3, 4, 5	3imtr4i 280	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ⊆ wss 3540   ∘ ccom 5042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-co 5047

This theorem is referenced by:  coeq1i  5203  coeq1d  5205  coi2  5569  relcnvtr  5572  funcoeqres  6080  ereq1  7636  domssex2  8005  wemapwe  8477  seqf1olem2  12703  seqf1o  12704  relexpsucnnl  13620  isps  17025  pwsco1mhm  17193  frmdup3  17227  symgov  17633  pmtr3ncom  17718  psgnunilem1  17736  frgpup3  18014  gsumval3  18131  evlseu  19337  evlsval2  19341  evls1val  19506  evls1sca  19509  evl1val  19514  mpfpf1  19536  pf1mpf  19537  pf1ind  19540  frgpcyg  19741  frlmup4  19959  xkococnlem  21272  xkococn  21273  cnmpt1k  21295  cnmptkk  21296  xkofvcn  21297  qtopeu  21329  qtophmeo  21430  utop2nei  21864  cncombf  23231  dgrcolem2  23834  dgrco  23835  motplusg  25237  hocsubdir  28028  hoddi  28233  opsqrlem1  28383  smatfval  29189  msubco  30682  trljco  35046  tgrpov  35054  tendovalco  35071  erngmul  35112  erngmul-rN  35120  cdlemksv  35150  cdlemkuu  35201  cdlemk41  35226  cdleml5N  35286  cdleml9  35290  dvamulr  35318  dvavadd  35321  dvhmulr  35393  dvhvscacbv  35405  dvhvscaval  35406  dih1dimatlem0  35635  dihjatcclem4  35728  diophrw  36340  eldioph2  36343  diophren  36395  mendmulr  36777  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848