![]() |
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 5802 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 “ cima 5446 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-br 4963 df-opab 5025 df-xp 5449 df-cnv 5451 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 |
This theorem is referenced by: cnvimarndm 5826 dmco 5982 imain 6309 fnimapr 6614 ssimaex 6615 intpreima 6703 resfunexg 6844 imauni 6870 isoini2 6955 frnsuppeq 7693 imacosuppOLD 7726 uniqs 8207 fiint 8641 jech9.3 9089 infxpenlem 9285 hsmexlem4 9697 frnnn0supp 11801 hashkf 13542 ghmeqker 18126 gsumval3lem1 18746 gsumval3lem2 18747 islinds2 20639 lindsind2 20645 snclseqg 22407 retopbas 23052 ismbf3d 23938 i1fima 23962 i1fd 23965 itg1addlem5 23984 limciun 24175 plyeq0 24484 spthispth 27194 0pth 27591 1pthdlem2 27602 eupth2lemb 27704 htth 28386 fcoinver 30047 fnimatp 30113 ffs2 30152 ffsrn 30153 tocyccntz 30423 sibfof 31215 eulerpartgbij 31247 eulerpartlemmf 31250 eulerpartlemgh 31253 eulerpart 31257 fiblem 31273 orrvcval4 31339 cvmsss2 32130 opelco3 32627 madeval2 32900 poimirlem3 34445 poimirlem30 34472 mbfposadd 34489 itg2addnclem2 34494 ftc1anclem5 34521 ftc1anclem6 34522 uniqsALTV 35137 pwfi2f1o 39200 brtrclfv2 39576 binomcxp 40246 |
Copyright terms: Public domain | W3C validator |