![]() |
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 5624 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) | |
2 | 1 | rneqd 5585 | . 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵)) |
3 | df-ima 5355 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
4 | df-ima 5355 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
5 | 2, 3, 4 | 3eqtr4g 2886 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ran crn 5343 ↾ cres 5344 “ cima 5345 |
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 2803 |
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 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-br 4874 df-opab 4936 df-xp 5348 df-cnv 5350 df-dm 5352 df-rn 5353 df-res 5354 df-ima 5355 |
This theorem is referenced by: imaeq2i 5705 imaeq2d 5707 relimasn 5729 funimaexg 6208 fimadmfo 6362 ssimaex 6510 ssimaexg 6511 isoselem 6846 isowe2 6855 f1opw2 7148 fnse 7558 supp0cosupp0 7599 tz7.49 7806 ecexr 8014 fopwdom 8337 sbthlem2 8340 sbth 8349 ssenen 8403 domunfican 8502 fodomfi 8508 f1opwfi 8539 fipreima 8541 marypha1lem 8608 ordtypelem2 8693 ordtypelem3 8694 ordtypelem9 8700 dfac12lem2 9281 dfac12r 9283 ackbij2lem2 9377 ackbij2lem3 9378 r1om 9381 enfin2i 9458 zorn2lem6 9638 zorn2lem7 9639 isacs5lem 17522 acsdrscl 17523 gicsubgen 18071 efgrelexlema 18515 tgcn 21427 subbascn 21429 iscnp4 21438 cnpnei 21439 cnima 21440 iscncl 21444 cncls 21449 cnconst2 21458 cnrest2 21461 cnprest 21464 cnindis 21467 cncmp 21566 cmpfi 21582 2ndcomap 21632 ptbasfi 21755 xkoopn 21763 xkoccn 21793 txcnp 21794 ptcnplem 21795 txcnmpt 21798 ptrescn 21813 xkoco1cn 21831 xkoco2cn 21832 xkococn 21834 xkoinjcn 21861 elqtop 21871 qtopomap 21892 qtopcmap 21893 ordthmeolem 21975 fbasrn 22058 elfm 22121 elfm2 22122 elfm3 22124 imaelfm 22125 rnelfmlem 22126 rnelfm 22127 fmfnfmlem2 22129 fmfnfmlem3 22130 fmfnfmlem4 22131 fmco 22135 flffbas 22169 lmflf 22179 fcfneii 22211 ptcmplem3 22228 ptcmplem5 22230 ptcmpg 22231 cnextcn 22241 symgtgp 22275 ghmcnp 22288 eltsms 22306 tsmsf1o 22318 fmucnd 22466 ucnextcn 22478 metcnp3 22715 mbfdm 23792 ismbf 23794 mbfima 23796 ismbfd 23805 mbfimaopnlem 23821 mbfimaopn2 23823 i1fd 23847 ellimc2 24040 limcflf 24044 xrlimcnp 25108 ubthlem1 28281 disjpreima 29944 imadifxp 29961 qtophaus 30448 rrhre 30610 mbfmcnvima 30864 imambfm 30869 eulerpartgbij 30979 erdszelem1 31719 erdsze 31730 erdsze2lem2 31732 cvmscbv 31786 cvmsi 31793 cvmsval 31794 cvmliftlem15 31826 opelco3 32216 brimageg 32573 fnimage 32575 imageval 32576 fvimage 32577 filnetlem4 32914 ptrest 33952 ismtyhmeolem 34145 ismtybndlem 34147 heibor1lem 34150 lmhmfgima 38497 brtrclfv2 38860 csbfv12gALTVD 39953 icccncfext 40895 sge0f1o 41390 smfresal 41789 smfpimbor1lem1 41799 smfpimbor1lem2 41800 smfco 41803 isomushgr 42544 isomuspgrlem1 42545 isomuspgrlem2a 42546 isomuspgrlem2b 42547 isomuspgrlem2c 42548 isomuspgrlem2d 42549 isomuspgr 42552 isomgrsym 42554 |
Copyright terms: Public domain | W3C validator |