Theorem coeq2 5808

Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)

Assertion

Ref	Expression
coeq2	⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Proof of Theorem coeq2

Step	Hyp	Ref	Expression
1		coss2 5806	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
2		coss2 5806	. . 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:  coeq2i  5810  coeq2d  5812  coi2  6223  f1eqcocnv  7250  ereq1  8645  dfttrcl2  9639  seqf1olem2  13998  seqf1o  13999  relexpsucnnr  14981  isps  18528  pwsco2mhm  18795  gsumwmhm  18807  frmdgsum  18824  frmdup1  18826  frmdup2  18827  efmndov  18843  symggrplem  18846  smndex1mndlem  18874  smndex1mnd  18875  pmtr3ncom  19444  psgnunilem1  19462  frgpuplem  19741  frgpupf  19742  frgpupval  19743  gsumval3eu  19873  gsumval3lem2  19875  rngcinv  20608  ringcinv  20642  selvval  22114  rhmmpl  22361  rhmply1vr1  22365  rhmply1vsca  22366  kgencn2  23535  upxp  23601  uptx  23603  txcn  23604  xkococnlem  23637  xkococn  23638  cnmptk1  23659  cnmptkk  23661  xkofvcn  23662  imasdsf1olem  24351  pi1cof  25039  pi1coval  25040  elovolmr  25456  ovoliunlem3  25484  ismbf1  25604  motplusg  28627  hocsubdir  31874  hoddi  32079  lnopco0i  32093  opsqrlem1  32229  pjsdi2i  32246  pjin2i  32282  pjclem1  32284  symgfcoeu  33161  1arithidomlem1  33613  1arithidom  33615  mplvrpmfgalem  33706  mplvrpmga  33707  mplvrpmmhm  33708  mplvrpmrhm  33709  splysubrg  33722  issply  33723  eulerpartgbij  34535  cvmliftmo  35485  cvmliftlem14  35498  cvmliftiota  35502  cvmlift2lem13  35516  cvmlift2  35517  cvmliftphtlem  35518  cvmlift3lem2  35521  cvmlift3lem6  35525  cvmlift3lem7  35526  cvmlift3lem9  35528  cvmlift3  35529  msubco  35732  ftc1anclem8  38038  upixp  38067  coideq  38586  xrneq1  38734  xrneq2  38737  shiftstableeq2  38821  trlcoat  41186  trljco  41203  tgrpov  41211  tendovalco  41228  erngmul  41269  erngmul-rN  41277  dvamulr  41475  dvavadd  41478  dvhmulr  41549  dihjatcclem4  41884  rhmpsr  43012  mendmulr  43633  hoiprodcl2  47004  ovnlecvr  47007  ovncvrrp  47013  ovnsubaddlem2  47020  ovncvr2  47060  opnvonmbllem1  47081  opnvonmbl  47083  ovolval4lem2  47099  ovolval5lem2  47102  ovolval5lem3  47103  ovolval5  47104  ovnovollem2  47106  rngcinvALTV  48767  ringcinvALTV  48801  itcoval1  49154  itcoval2  49155  itcoval3  49156  itcovalsucov  49159