Theorem coeq1 5871

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3963   ∘ ccom 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-br 5149  df-opab 5211  df-co 5698

This theorem is referenced by:  coeq1i  5873  coeq1d  5875  coi2  6285  funcoeqres  6880  wrecseq123  8338  ereq1  8751  domssex2  9176  wemapwe  9735  dfttrcl2  9762  updjud  9972  seqf1olem2  14080  seqf1o  14081  relexpsucnnl  15066  isps  18626  pwsco1mhm  18858  frmdup3  18893  efmndov  18907  symggrplem  18910  smndex1mndlem  18935  smndex1mnd  18936  pmtr3ncom  19508  psgnunilem1  19526  frgpup3  19811  gsumval3  19940  rngcinv  20654  ringcinv  20688  frgpcyg  21610  frlmup4  21839  evlseu  22125  evlsval2  22129  selvval  22157  evls1val  22340  evls1sca  22343  evl1val  22349  mpfpf1  22371  pf1mpf  22372  pf1ind  22375  xkococnlem  23683  xkococn  23684  cnmpt1k  23706  cnmptkk  23707  xkofvcn  23708  qtopeu  23740  qtophmeo  23841  utop2nei  24275  cncombf  25707  dgrcolem2  26329  dgrco  26330  motplusg  28565  hocsubdir  31814  hoddi  32019  opsqrlem1  32169  1arithidom  33545  smatfval  33756  msubco  35516  coideq  38228  trljco  40723  tgrpov  40731  tendovalco  40748  erngmul  40789  erngmul-rN  40797  cdlemksv  40827  cdlemkuu  40878  cdlemk41  40903  cdleml5N  40963  cdleml9  40967  dvamulr  40995  dvavadd  40998  dvhmulr  41069  dvhvscacbv  41081  dvhvscaval  41082  dih1dimatlem0  41311  dihjatcclem4  41404  evlsval3  42546  diophrw  42747  eldioph2  42750  diophren  42801  mendmulr  43173  fundcmpsurinjpreimafv  47333  rngcinvALTV  48120  ringcinvALTV  48154  itcoval  48511