Theorem coeq2 5437

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 5435	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
2		coss2 5435	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴))
3	1, 2	anim12i 591	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
4		eqss 3760	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3760	. 2 ⊢ ((𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) ↔ ((𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵) ∧ (𝐶 ∘ 𝐵) ⊆ (𝐶 ∘ 𝐴)))
6	3, 4, 5	3imtr4i 281	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ⊆ wss 3716   ∘ ccom 5271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-in 3723  df-ss 3730  df-br 4806  df-opab 4866  df-co 5276

This theorem is referenced by:  coeq2i  5439  coeq2d  5441  coi2  5814  relcnvtr  5817  f1eqcocnv  6721  ereq1  7921  seqf1olem2  13056  seqf1o  13057  relexpsucnnr  13985  isps  17424  pwsco2mhm  17593  gsumwmhm  17604  frmdgsum  17621  frmdup1  17623  frmdup2  17624  symgov  18031  pmtr3ncom  18116  psgnunilem1  18134  frgpuplem  18406  frgpupf  18407  frgpupval  18408  gsumval3eu  18526  gsumval3lem2  18528  kgencn2  21583  upxp  21649  uptx  21651  txcn  21652  xkococnlem  21685  xkococn  21686  cnmptk1  21707  cnmptkk  21709  xkofvcn  21710  imasdsf1olem  22400  pi1cof  23080  pi1coval  23081  elovolmr  23465  ovoliunlem3  23493  ismbf1  23613  motplusg  25658  hocsubdir  28975  hoddi  29180  lnopco0i  29194  opsqrlem1  29330  pjsdi2i  29347  pjin2i  29383  pjclem1  29385  symgfcoeu  30176  eulerpartgbij  30765  cvmliftmo  31595  cvmliftlem14  31608  cvmliftiota  31612  cvmlift2lem13  31626  cvmlift2  31627  cvmliftphtlem  31628  cvmlift3lem2  31631  cvmlift3lem6  31635  cvmlift3lem7  31636  cvmlift3lem9  31638  cvmlift3  31639  msubco  31757  ftc1anclem8  33824  upixp  33856  coideq  34353  xrneq1  34481  xrneq2  34484  trlcoat  36532  trljco  36549  tgrpov  36557  tendovalco  36574  erngmul  36615  erngmul-rN  36623  dvamulr  36821  dvavadd  36824  dvhmulr  36896  dihjatcclem4  37231  mendmulr  38279  hoiprodcl2  41294  ovnlecvr  41297  ovncvrrp  41303  ovnsubaddlem2  41310  ovncvr2  41350  opnvonmbllem1  41371  opnvonmbl  41373  ovolval4lem2  41389  ovolval5lem2  41392  ovolval5lem3  41393  ovolval5  41394  ovnovollem2  41396  rngcinv  42510  rngcinvALTV  42522  ringcinv  42561  ringcinvALTV  42585