![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imaeq12d | Structured version Visualization version GIF version |
Description: Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.) |
Ref | Expression |
---|---|
imaeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
imaeq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
imaeq12d | ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imaeq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | imaeq1d 5895 | . 2 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) |
3 | imaeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | imaeq2d 5896 | . 2 ⊢ (𝜑 → (𝐵 “ 𝐶) = (𝐵 “ 𝐷)) |
5 | 2, 4 | eqtrd 2833 | 1 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 “ cima 5522 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-rab 3115 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 df-xp 5525 df-cnv 5527 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 |
This theorem is referenced by: csbima12 5914 predeq123 6117 vdwpc 16306 dmdprd 19113 isunit 19403 qtopval 22300 limciun 24497 ig1pval 24773 ispth 27512 qqhval 31325 eulerpartgbij 31740 orvcval 31825 ballotlemrval 31885 ballotlemrinv0 31900 ballotlemrinv 31901 mthmval 32935 bj-projeq 34428 itg2addnclem2 35109 islmodfg 40013 heeq12 40477 |
Copyright terms: Public domain | W3C validator |