Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > imaeq2i | Structured version Visualization version GIF version |
Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
Ref | Expression |
---|---|
imaeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
imaeq2i | ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imaeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | imaeq2 5925 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 “ cima 5558 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-br 5067 df-opab 5129 df-xp 5561 df-cnv 5563 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 |
This theorem is referenced by: cnvimarndm 5950 dmco 6107 imain 6439 fnimapr 6747 ssimaex 6748 intpreima 6838 resfunexg 6978 imauni 7005 isoini2 7092 frnsuppeq 7842 imacosuppOLD 7875 uniqs 8357 fiint 8795 jech9.3 9243 infxpenlem 9439 hsmexlem4 9851 frnnn0supp 11954 hashkf 13693 ghmeqker 18385 gsumval3lem1 19025 gsumval3lem2 19026 islinds2 20957 lindsind2 20963 snclseqg 22724 retopbas 23369 ismbf3d 24255 i1fima 24279 i1fd 24282 itg1addlem5 24301 limciun 24492 plyeq0 24801 spthispth 27507 0pth 27904 1pthdlem2 27915 eupth2lemb 28016 htth 28695 fcoinver 30357 fnimatp 30423 ffs2 30464 ffsrn 30465 tocyccntz 30786 sibfof 31598 eulerpartgbij 31630 eulerpartlemmf 31633 eulerpartlemgh 31636 eulerpart 31640 fiblem 31656 orrvcval4 31722 cvmsss2 32521 opelco3 33018 madeval2 33290 poimirlem3 34910 poimirlem30 34937 mbfposadd 34954 itg2addnclem2 34959 ftc1anclem5 34986 ftc1anclem6 34987 uniqsALTV 35601 pwfi2f1o 39716 brtrclfv2 40092 binomcxp 40709 |
Copyright terms: Public domain | W3C validator |