Theorem coeq1 5513

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1658   ⊆ wss 3799   ∘ ccom 5347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-in 3806  df-ss 3813  df-br 4875  df-opab 4937  df-co 5352

This theorem is referenced by:  coeq1i  5515  coeq1d  5517  coi2  5894  relcnvtr  5897  funcoeqres  6409  ereq1  8017  domssex2  8390  wemapwe  8872  updjud  9074  seqf1olem2  13136  seqf1o  13137  relexpsucnnl  14150  isps  17556  pwsco1mhm  17724  frmdup3  17759  symgov  18161  pmtr3ncom  18246  psgnunilem1  18264  frgpup3  18545  gsumval3  18662  evlseu  19877  evlsval2  19881  evls1val  20046  evls1sca  20049  evl1val  20054  mpfpf1  20076  pf1mpf  20077  pf1ind  20080  frgpcyg  20282  frlmup4  20508  xkococnlem  21834  xkococn  21835  cnmpt1k  21857  cnmptkk  21858  xkofvcn  21859  qtopeu  21891  qtophmeo  21992  utop2nei  22425  cncombf  23825  dgrcolem2  24430  dgrco  24431  motplusg  25855  hocsubdir  29200  hoddi  29405  opsqrlem1  29555  smatfval  30407  msubco  31975  coideq  34565  trljco  36816  tgrpov  36824  tendovalco  36841  erngmul  36882  erngmul-rN  36890  cdlemksv  36920  cdlemkuu  36971  cdlemk41  36996  cdleml5N  37056  cdleml9  37060  dvamulr  37088  dvavadd  37091  dvhmulr  37162  dvhvscacbv  37174  dvhvscaval  37175  dih1dimatlem0  37404  dihjatcclem4  37497  diophrw  38167  eldioph2  38170  diophren  38222  mendmulr  38602  rngcinv  42829  rngcinvALTV  42841  ringcinv  42880  ringcinvALTV  42904