Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > imaeq2 | Structured version Visualization version GIF version |
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
imaeq2 | ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseq2 5842 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) | |
2 | 1 | rneqd 5802 | . 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵)) |
3 | df-ima 5562 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
4 | df-ima 5562 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
5 | 2, 3, 4 | 3eqtr4g 2881 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ran crn 5550 ↾ cres 5551 “ cima 5552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 df-opab 5121 df-xp 5555 df-cnv 5557 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 |
This theorem is referenced by: imaeq2i 5921 imaeq2d 5923 relimasn 5946 funimaexg 6434 fimadmfo 6593 ssimaex 6742 ssimaexg 6743 isoselem 7083 isowe2 7092 f1opw2 7389 fnse 7818 supp0cosupp0 7863 supp0cosupp0OLD 7864 tz7.49 8072 ecexr 8284 fopwdom 8614 sbthlem2 8617 sbth 8626 ssenen 8680 domunfican 8780 fodomfi 8786 f1opwfi 8817 fipreima 8819 marypha1lem 8886 ordtypelem2 8972 ordtypelem3 8973 ordtypelem9 8979 dfac12lem2 9559 dfac12r 9561 ackbij2lem2 9651 ackbij2lem3 9652 r1om 9655 enfin2i 9732 zorn2lem6 9912 zorn2lem7 9913 isacs5lem 17769 acsdrscl 17770 gicsubgen 18358 efgrelexlema 18806 tgcn 21790 subbascn 21792 iscnp4 21801 cnpnei 21802 cnima 21803 iscncl 21807 cncls 21812 cnconst2 21821 cnrest2 21824 cnprest 21827 cnindis 21830 cncmp 21930 cmpfi 21946 2ndcomap 21996 ptbasfi 22119 xkoopn 22127 xkoccn 22157 txcnp 22158 ptcnplem 22159 txcnmpt 22162 ptrescn 22177 xkoco1cn 22195 xkoco2cn 22196 xkococn 22198 xkoinjcn 22225 elqtop 22235 qtopomap 22256 qtopcmap 22257 ordthmeolem 22339 fbasrn 22422 elfm 22485 elfm2 22486 elfm3 22488 imaelfm 22489 rnelfmlem 22490 rnelfm 22491 fmfnfmlem2 22493 fmfnfmlem3 22494 fmfnfmlem4 22495 fmco 22499 flffbas 22533 lmflf 22543 fcfneii 22575 ptcmplem3 22592 ptcmplem5 22594 ptcmpg 22595 cnextcn 22605 symgtgp 22639 ghmcnp 22652 eltsms 22670 tsmsf1o 22682 fmucnd 22830 ucnextcn 22842 metcnp3 23079 mbfdm 24156 ismbf 24158 mbfima 24160 ismbfd 24169 mbfimaopnlem 24185 mbfimaopn2 24187 i1fd 24211 ellimc2 24404 limcflf 24408 xrlimcnp 25474 ubthlem1 28575 disjpreima 30263 imadifxp 30280 preimane 30344 fnpreimac 30345 qtophaus 31000 rrhre 31162 mbfmcnvima 31415 imambfm 31420 eulerpartgbij 31530 erdszelem1 32336 erdsze 32347 erdsze2lem2 32349 cvmscbv 32403 cvmsi 32410 cvmsval 32411 cvmliftlem15 32443 opelco3 32916 brimageg 33286 fnimage 33288 imageval 33289 fvimage 33290 filnetlem4 33627 bj-imdirval3 34367 ptrest 34773 ismtyhmeolem 34965 ismtybndlem 34967 heibor1lem 34970 lmhmfgima 39564 brtrclfv2 39952 csbfv12gALTVD 41113 icccncfext 42050 sge0f1o 42545 smfresal 42944 smfpimbor1lem1 42954 smfpimbor1lem2 42955 smfco 42958 isomushgr 43838 isomuspgrlem1 43839 isomuspgrlem2a 43840 isomuspgrlem2b 43841 isomuspgrlem2c 43842 isomuspgrlem2d 43843 isomuspgr 43846 isomgrsym 43848 |
Copyright terms: Public domain | W3C validator |