Theorem coeq1 5450

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1652   ⊆ wss 3734   ∘ ccom 5283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-in 3741  df-ss 3748  df-br 4812  df-opab 4874  df-co 5288

This theorem is referenced by:  coeq1i  5452  coeq1d  5454  coi2  5840  relcnvtr  5843  funcoeqres  6352  ereq1  7956  domssex2  8329  wemapwe  8811  updjud  9013  seqf1olem2  13051  seqf1o  13052  relexpsucnnl  14060  isps  17471  pwsco1mhm  17639  frmdup3  17674  symgov  18076  pmtr3ncom  18161  psgnunilem1  18179  frgpup3  18460  gsumval3  18577  evlseu  19792  evlsval2  19796  evls1val  19961  evls1sca  19964  evl1val  19969  mpfpf1  19991  pf1mpf  19992  pf1ind  19995  frgpcyg  20197  frlmup4  20419  xkococnlem  21745  xkococn  21746  cnmpt1k  21768  cnmptkk  21769  xkofvcn  21770  qtopeu  21802  qtophmeo  21903  utop2nei  22336  cncombf  23719  dgrcolem2  24324  dgrco  24325  motplusg  25731  hocsubdir  29103  hoddi  29308  opsqrlem1  29458  smatfval  30311  msubco  31879  coideq  34448  trljco  36699  tgrpov  36707  tendovalco  36724  erngmul  36765  erngmul-rN  36773  cdlemksv  36803  cdlemkuu  36854  cdlemk41  36879  cdleml5N  36939  cdleml9  36943  dvamulr  36971  dvavadd  36974  dvhmulr  37045  dvhvscacbv  37057  dvhvscaval  37058  dih1dimatlem0  37287  dihjatcclem4  37380  diophrw  38003  eldioph2  38006  diophren  38058  mendmulr  38438  rngcinv  42653  rngcinvALTV  42665  ringcinv  42704  ringcinvALTV  42728