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

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

Proof of Theorem imaeq1
StepHypRef Expression
1 reseq1 5840 . . 3 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
21rneqd 5801 . 2 (𝐴 = 𝐵 → ran (𝐴𝐶) = ran (𝐵𝐶))
3 df-ima 5561 . 2 (𝐴𝐶) = ran (𝐴𝐶)
4 df-ima 5561 . 2 (𝐵𝐶) = ran (𝐵𝐶)
52, 3, 43eqtr4g 2879 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  ran crn 5549  cres 5550  cima 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561
This theorem is referenced by:  imaeq1i  5919  imaeq1d  5921  suppval  7824  eceq2  8321  marypha1lem  8889  marypha1  8890  ackbij2lem2  9654  ackbij2lem3  9655  r1om  9658  limsupval  14823  isacs1i  16920  mreacs  16921  islindf  20948  iscnp  21837  xkoccn  22219  xkohaus  22253  xkoco1cn  22257  xkoco2cn  22258  xkococnlem  22259  xkococn  22260  xkoinjcn  22287  fmval  22543  fmf  22545  utoptop  22835  restutop  22838  restutopopn  22839  ustuqtoplem  22840  ustuqtop1  22842  ustuqtop2  22843  ustuqtop4  22845  ustuqtop5  22846  utopsnneiplem  22848  utopsnnei  22850  neipcfilu  22897  psmetutop  23169  cfilfval  23859  elply2  24778  coeeu  24807  coelem  24808  coeeq  24809  dmarea  25527  mclsax  32809  tailfval  33713  bj-cleq  34267  bj-funun  34526  poimirlem15  34899  poimirlem24  34908  brtrclfv2  40062  liminfval  42029  isomgreqve  43980  isomgrsym  43991  isomgrtr  43994  ushrisomgr  43996
  Copyright terms: Public domain W3C validator