Theorem coeq1 5811

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-co 5640

This theorem is referenced by:  coeq1i  5813  coeq1d  5815  coi2  6224  funcoeqres  6813  wrecseq123  8269  ereq1  8655  domssex2  9078  wemapwe  9626  dfttrcl2  9653  updjud  9863  seqf1olem2  13983  seqf1o  13984  relexpsucnnl  14972  isps  18503  pwsco1mhm  18735  frmdup3  18770  efmndov  18784  symggrplem  18787  smndex1mndlem  18812  smndex1mnd  18813  pmtr3ncom  19381  psgnunilem1  19399  frgpup3  19684  gsumval3  19813  rngcinv  20522  ringcinv  20556  frgpcyg  21459  frlmup4  21686  evlseu  21966  evlsval2  21970  selvval  21998  evls1val  22183  evls1sca  22186  evl1val  22192  mpfpf1  22214  pf1mpf  22215  pf1ind  22218  xkococnlem  23522  xkococn  23523  cnmpt1k  23545  cnmptkk  23546  xkofvcn  23547  qtopeu  23579  qtophmeo  23680  utop2nei  24114  cncombf  25535  dgrcolem2  26156  dgrco  26157  motplusg  28445  hocsubdir  31687  hoddi  31892  opsqrlem1  32042  1arithidom  33481  smatfval  33758  msubco  35491  coideq  38208  trljco  40707  tgrpov  40715  tendovalco  40732  erngmul  40773  erngmul-rN  40781  cdlemksv  40811  cdlemkuu  40862  cdlemk41  40887  cdleml5N  40947  cdleml9  40951  dvamulr  40979  dvavadd  40982  dvhmulr  41053  dvhvscacbv  41065  dvhvscaval  41066  dih1dimatlem0  41295  dihjatcclem4  41388  evlsval3  42520  diophrw  42720  eldioph2  42723  diophren  42774  mendmulr  43146  fundcmpsurinjpreimafv  47382  rngcinvALTV  48237  ringcinvALTV  48271  itcoval  48623  setc1ocofval  49456