Theorem coeq1 5806

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-br 5099  df-opab 5161  df-co 5633

This theorem is referenced by:  coeq1i  5808  coeq1d  5810  coi2  6222  funcoeqres  6805  wrecseq123  8255  ereq1  8642  domssex2  9065  wemapwe  9606  dfttrcl2  9633  updjud  9846  seqf1olem2  13965  seqf1o  13966  relexpsucnnl  14953  isps  18491  pwsco1mhm  18757  frmdup3  18792  efmndov  18806  symggrplem  18809  smndex1mndlem  18834  smndex1mnd  18835  pmtr3ncom  19404  psgnunilem1  19422  frgpup3  19707  gsumval3  19836  rngcinv  20570  ringcinv  20604  frgpcyg  21528  frlmup4  21756  evlseu  22038  evlsval2  22042  evlsval3  22044  selvval  22078  evls1val  22264  evls1sca  22267  evl1val  22273  mpfpf1  22295  pf1mpf  22296  pf1ind  22299  xkococnlem  23603  xkococn  23604  cnmpt1k  23626  cnmptkk  23627  xkofvcn  23628  qtopeu  23660  qtophmeo  23761  utop2nei  24194  cncombf  25615  dgrcolem2  26236  dgrco  26237  motplusg  28614  hocsubdir  31860  hoddi  32065  opsqrlem1  32215  1arithidom  33618  mplvrpmga  33710  mplvrpmrhm  33712  issply  33719  smatfval  33952  msubco  35725  coideq  38444  trljco  41000  tgrpov  41008  tendovalco  41025  erngmul  41066  erngmul-rN  41074  cdlemksv  41104  cdlemkuu  41155  cdlemk41  41180  cdleml5N  41240  cdleml9  41244  dvamulr  41272  dvavadd  41275  dvhmulr  41346  dvhvscacbv  41358  dvhvscaval  41359  dih1dimatlem0  41588  dihjatcclem4  41681  diophrw  43001  eldioph2  43004  diophren  43055  mendmulr  43426  fundcmpsurinjpreimafv  47654  rngcinvALTV  48522  ringcinvALTV  48556  itcoval  48907  setc1ocofval  49739