![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imaeq1i | Structured version Visualization version GIF version |
Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
Ref | Expression |
---|---|
imaeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
imaeq1i | ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imaeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | imaeq1 5703 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 “ cima 5346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4875 df-opab 4937 df-cnv 5351 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 |
This theorem is referenced by: mptpreima 5870 isarep2 6212 suppun 7580 supp0cosupp0 7600 imacosupp 7601 fsuppun 8564 fsuppcolem 8576 marypha2lem4 8614 dfoi 8686 r1limg 8912 isf34lem3 9513 compss 9514 fpwwe2lem13 9780 infrenegsup 11337 gsumzf1o 18667 ssidcn 21431 cnco 21442 qtopres 21873 idqtop 21881 qtopcn 21889 mbfid 23802 mbfres 23811 cncombf 23825 dvlog 24797 efopnlem2 24803 eucrct2eupthOLD 27624 eucrct2eupth 27625 disjpreima 29945 imadifxp 29962 rinvf1o 29982 mbfmcst 30867 mbfmco 30872 sitmcl 30959 eulerpartlemt 30979 eulerpartlemmf 30983 eulerpart 30990 0rrv 31060 mclsppslem 32027 csbpredg 33719 mptsnun 33733 poimirlem3 33957 ftc1anclem3 34031 areacirclem5 34048 cytpval 38631 arearect 38644 brtrclfv2 38861 0cnf 40886 fourierdlem62 41180 smfco 41804 |
Copyright terms: Public domain | W3C validator |