MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imaeq1 Structured version   Visualization version   GIF version

Theorem imaeq1 5676
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
imaeq1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem imaeq1
StepHypRef Expression
1 reseq1 5592 . . 3 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
21rneqd 5554 . 2 (𝐴 = 𝐵 → ran (𝐴𝐶) = ran (𝐵𝐶))
3 df-ima 5323 . 2 (𝐴𝐶) = ran (𝐴𝐶)
4 df-ima 5323 . 2 (𝐵𝐶) = ran (𝐵𝐶)
52, 3, 43eqtr4g 2856 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  ran crn 5311  cres 5312  cima 5313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-br 4842  df-opab 4904  df-cnv 5318  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323
This theorem is referenced by:  imaeq1i  5678  imaeq1d  5680  suppval  7532  eceq2  8020  marypha1lem  8579  marypha1  8580  ackbij2lem2  9348  ackbij2lem3  9349  r1om  9352  limsupval  14543  isacs1i  16629  mreacs  16630  islindf  20473  iscnp  21367  xkoccn  21748  xkohaus  21782  xkoco1cn  21786  xkoco2cn  21787  xkococnlem  21788  xkococn  21789  xkoinjcn  21816  fmval  22072  fmf  22074  utoptop  22363  restutop  22366  restutopopn  22367  ustuqtoplem  22368  ustuqtop1  22370  ustuqtop2  22371  ustuqtop4  22373  ustuqtop5  22374  utopsnneiplem  22376  utopsnnei  22378  neipcfilu  22425  psmetutop  22697  cfilfval  23387  elply2  24290  coeeu  24319  coelem  24320  coeeq  24321  dmarea  25033  mclsax  31975  tailfval  32871  bj-cleq  33433  poimirlem15  33905  poimirlem24  33914  brtrclfv2  38790  liminfval  40723  isomgreqve  42483  isomgrsym  42494  isomgrtr  42497  ushrisomgr  42499
  Copyright terms: Public domain W3C validator