Theorem coeq1 5807

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3890   ∘ ccom 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-co 5634

This theorem is referenced by:  coeq1i  5809  coeq1d  5811  coi2  6223  funcoeqres  6806  wrecseq123  8257  ereq1  8645  domssex2  9069  wemapwe  9612  dfttrcl2  9639  updjud  9852  seqf1olem2  13998  seqf1o  13999  relexpsucnnl  14986  isps  18528  pwsco1mhm  18794  frmdup3  18829  efmndov  18843  symggrplem  18846  smndex1mndlem  18874  smndex1mnd  18875  pmtr3ncom  19444  psgnunilem1  19462  frgpup3  19747  gsumval3  19876  rngcinv  20608  ringcinv  20642  frgpcyg  21566  frlmup4  21794  evlseu  22074  evlsval2  22078  evlsval3  22080  selvval  22114  evls1val  22298  evls1sca  22301  evl1val  22307  mpfpf1  22329  pf1mpf  22330  pf1ind  22333  xkococnlem  23637  xkococn  23638  cnmpt1k  23660  cnmptkk  23661  xkofvcn  23662  qtopeu  23694  qtophmeo  23795  utop2nei  24228  cncombf  25638  dgrcolem2  26252  dgrco  26253  motplusg  28627  hocsubdir  31874  hoddi  32079  opsqrlem1  32229  1arithidom  33615  mplvrpmga  33707  mplvrpmrhm  33709  issply  33723  smatfval  33958  msubco  35732  coideq  38586  trljco  41203  tgrpov  41211  tendovalco  41228  erngmul  41269  erngmul-rN  41277  cdlemksv  41307  cdlemkuu  41358  cdlemk41  41383  cdleml5N  41443  cdleml9  41447  dvamulr  41475  dvavadd  41478  dvhmulr  41549  dvhvscacbv  41561  dvhvscaval  41562  dih1dimatlem0  41791  dihjatcclem4  41884  diophrw  43208  eldioph2  43211  diophren  43262  mendmulr  43633  fundcmpsurinjpreimafv  47883  rngcinvALTV  48767  ringcinvALTV  48801  itcoval  49152  setc1ocofval  49984