Theorem coeq1 5812

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-co 5640

This theorem is referenced by:  coeq1i  5814  coeq1d  5816  coi2  6228  funcoeqres  6811  wrecseq123  8263  ereq1  8651  domssex2  9075  wemapwe  9618  dfttrcl2  9645  updjud  9858  seqf1olem2  14004  seqf1o  14005  relexpsucnnl  14992  isps  18534  pwsco1mhm  18800  frmdup3  18835  efmndov  18849  symggrplem  18852  smndex1mndlem  18880  smndex1mnd  18881  pmtr3ncom  19450  psgnunilem1  19468  frgpup3  19753  gsumval3  19882  rngcinv  20614  ringcinv  20648  frgpcyg  21553  frlmup4  21781  evlseu  22061  evlsval2  22065  evlsval3  22067  selvval  22101  evls1val  22285  evls1sca  22288  evl1val  22294  mpfpf1  22316  pf1mpf  22317  pf1ind  22320  xkococnlem  23624  xkococn  23625  cnmpt1k  23647  cnmptkk  23648  xkofvcn  23649  qtopeu  23681  qtophmeo  23782  utop2nei  24215  cncombf  25625  dgrcolem2  26239  dgrco  26240  motplusg  28610  hocsubdir  31856  hoddi  32061  opsqrlem1  32211  1arithidom  33597  mplvrpmga  33689  mplvrpmrhm  33691  issply  33705  smatfval  33939  msubco  35713  coideq  38569  trljco  41186  tgrpov  41194  tendovalco  41211  erngmul  41252  erngmul-rN  41260  cdlemksv  41290  cdlemkuu  41341  cdlemk41  41366  cdleml5N  41426  cdleml9  41430  dvamulr  41458  dvavadd  41461  dvhmulr  41532  dvhvscacbv  41544  dvhvscaval  41545  dih1dimatlem0  41774  dihjatcclem4  41867  diophrw  43191  eldioph2  43194  diophren  43241  mendmulr  43612  fundcmpsurinjpreimafv  47868  rngcinvALTV  48752  ringcinvALTV  48786  itcoval  49137  setc1ocofval  49969