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 5391 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) | |
2 | 1 | rneqd 5353 | . 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵)) |
3 | df-ima 5127 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
4 | df-ima 5127 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
5 | 2, 3, 4 | 3eqtr4g 2681 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1483 ran crn 5115 ↾ cres 5116 “ cima 5117 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-xp 5120 df-cnv 5122 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 |
This theorem is referenced by: imaeq2i 5464 imaeq2d 5466 relimasn 5488 funimaexg 5975 ssimaex 6263 ssimaexg 6264 isoselem 6591 isowe2 6600 f1opw2 6888 fnse 7294 supp0cosupp0 7334 tz7.49 7540 ecexr 7747 fopwdom 8068 sbthlem2 8071 sbth 8080 ssenen 8134 domunfican 8233 fodomfi 8239 f1opwfi 8270 fipreima 8272 marypha1lem 8339 ordtypelem2 8424 ordtypelem3 8425 ordtypelem9 8431 dfac12lem2 8966 dfac12r 8968 ackbij2lem2 9062 ackbij2lem3 9063 r1om 9066 enfin2i 9143 zorn2lem6 9323 zorn2lem7 9324 isacs5lem 17169 acsdrscl 17170 gicsubgen 17721 efgrelexlema 18162 tgcn 21056 subbascn 21058 iscnp4 21067 cnpnei 21068 cnima 21069 iscncl 21073 cncls 21078 cnconst2 21087 cnrest2 21090 cnprest 21093 cnindis 21096 cncmp 21195 cmpfi 21211 2ndcomap 21261 ptbasfi 21384 xkoopn 21392 xkoccn 21422 txcnp 21423 ptcnplem 21424 txcnmpt 21427 ptrescn 21442 xkoco1cn 21460 xkoco2cn 21461 xkococn 21463 xkoinjcn 21490 elqtop 21500 qtopomap 21521 qtopcmap 21522 ordthmeolem 21604 fbasrn 21688 elfm 21751 elfm2 21752 elfm3 21754 imaelfm 21755 rnelfmlem 21756 rnelfm 21757 fmfnfmlem2 21759 fmfnfmlem3 21760 fmfnfmlem4 21761 fmco 21765 flffbas 21799 lmflf 21809 fcfneii 21841 ptcmplem3 21858 ptcmplem5 21860 ptcmpg 21861 cnextcn 21871 symgtgp 21905 ghmcnp 21918 eltsms 21936 tsmsf1o 21948 fmucnd 22096 ucnextcn 22108 metcnp3 22345 mbfdm 23395 ismbf 23397 mbfima 23399 ismbfd 23407 mbfimaopnlem 23422 mbfimaopn2 23424 i1fd 23448 ellimc2 23641 limcflf 23645 xrlimcnp 24695 ubthlem1 27726 disjpreima 29397 imadifxp 29414 qtophaus 29903 rrhre 30065 mbfmcnvima 30319 imambfm 30324 eulerpartgbij 30434 erdszelem1 31173 erdsze 31184 erdsze2lem2 31186 cvmscbv 31240 cvmsi 31247 cvmsval 31248 cvmliftlem15 31280 opelco3 31678 brimageg 32034 fnimage 32036 imageval 32037 fvimage 32038 filnetlem4 32376 ptrest 33408 ismtyhmeolem 33603 ismtybndlem 33605 heibor1lem 33608 lmhmfgima 37654 brtrclfv2 38019 csbfv12gALTVD 39135 icccncfext 40100 sge0f1o 40599 smfresal 40995 smfpimbor1lem1 41005 smfpimbor1lem2 41006 smfco 41009 |
Copyright terms: Public domain | W3C validator |