Theorem coeq1 5868

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3951   ∘ ccom 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-co 5694

This theorem is referenced by:  coeq1i  5870  coeq1d  5872  coi2  6283  funcoeqres  6879  wrecseq123  8339  ereq1  8752  domssex2  9177  wemapwe  9737  dfttrcl2  9764  updjud  9974  seqf1olem2  14083  seqf1o  14084  relexpsucnnl  15069  isps  18613  pwsco1mhm  18845  frmdup3  18880  efmndov  18894  symggrplem  18897  smndex1mndlem  18922  smndex1mnd  18923  pmtr3ncom  19493  psgnunilem1  19511  frgpup3  19796  gsumval3  19925  rngcinv  20637  ringcinv  20671  frgpcyg  21592  frlmup4  21821  evlseu  22107  evlsval2  22111  selvval  22139  evls1val  22324  evls1sca  22327  evl1val  22333  mpfpf1  22355  pf1mpf  22356  pf1ind  22359  xkococnlem  23667  xkococn  23668  cnmpt1k  23690  cnmptkk  23691  xkofvcn  23692  qtopeu  23724  qtophmeo  23825  utop2nei  24259  cncombf  25693  dgrcolem2  26314  dgrco  26315  motplusg  28550  hocsubdir  31804  hoddi  32009  opsqrlem1  32159  1arithidom  33565  smatfval  33794  msubco  35536  coideq  38248  trljco  40742  tgrpov  40750  tendovalco  40767  erngmul  40808  erngmul-rN  40816  cdlemksv  40846  cdlemkuu  40897  cdlemk41  40922  cdleml5N  40982  cdleml9  40986  dvamulr  41014  dvavadd  41017  dvhmulr  41088  dvhvscacbv  41100  dvhvscaval  41101  dih1dimatlem0  41330  dihjatcclem4  41423  evlsval3  42569  diophrw  42770  eldioph2  42773  diophren  42824  mendmulr  43196  fundcmpsurinjpreimafv  47395  rngcinvALTV  48192  ringcinvALTV  48226  itcoval  48582