Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > coeq12d | Structured version Visualization version GIF version |
Description: Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
Ref | Expression |
---|---|
coeq12d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
coeq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
coeq12d | ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coeq12d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | coeq1d 5205 | . 2 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
3 | coeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | coeq2d 5206 | . 2 ⊢ (𝜑 → (𝐵 ∘ 𝐶) = (𝐵 ∘ 𝐷)) |
5 | 2, 4 | eqtrd 2644 | 1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∘ ccom 5042 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-in 3547 df-ss 3554 df-br 4584 df-opab 4644 df-co 5047 |
This theorem is referenced by: xpcoid 5593 dfac12lem1 8848 dfac12r 8851 trcleq2lem 13578 trclfvcotrg 13605 relexpaddg 13641 dfrtrcl2 13650 imasval 15994 cofuval 16365 cofu2nd 16368 cofuval2 16370 cofuass 16372 cofurid 16374 setcco 16556 estrcco 16593 funcestrcsetclem9 16611 funcsetcestrclem9 16626 isdir 17055 evl1fval 19513 znval 19702 znle2 19721 mdetfval 20211 mdetdiaglem 20223 ust0 21833 trust 21843 metustexhalf 22171 isngp 22210 ngppropd 22251 tngval 22253 tngngp2 22266 imsval 26924 opsqrlem3 28385 hmopidmch 28396 hmopidmpj 28397 pjidmco 28424 dfpjop 28425 zhmnrg 29339 istendo 35066 tendoco2 35074 tendoidcl 35075 tendococl 35078 tendoplcbv 35081 tendopl2 35083 tendoplco2 35085 tendodi1 35090 tendodi2 35091 tendo0co2 35094 tendoicl 35102 erngplus2 35110 erngplus2-rN 35118 cdlemk55u1 35271 cdlemk55u 35272 dvaplusgv 35316 dvhopvadd 35400 dvhlveclem 35415 dvhopaddN 35421 dicvaddcl 35497 dihopelvalcpre 35555 rtrclex 36943 trclubgNEW 36944 rtrclexi 36947 cnvtrcl0 36952 dfrtrcl5 36955 trcleq2lemRP 36956 csbcog 36960 trrelind 36976 trrelsuperreldg 36979 trficl 36980 trrelsuperrel2dg 36982 trclrelexplem 37022 relexpaddss 37029 dfrtrcl3 37044 clsneicnv 37423 neicvgnvo 37433 rngccoALTV 41780 funcrngcsetcALT 41791 funcringcsetcALTV2lem9 41836 ringccoALTV 41843 funcringcsetclem9ALTV 41859 |
Copyright terms: Public domain | W3C validator |