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

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

Proof of Theorem imaeq1
StepHypRef Expression
1 reseq1 5974 . . 3 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
21rneqd 5936 . 2 (𝐴 = 𝐵 → ran (𝐴𝐶) = ran (𝐵𝐶))
3 df-ima 5689 . 2 (𝐴𝐶) = ran (𝐴𝐶)
4 df-ima 5689 . 2 (𝐵𝐶) = ran (𝐵𝐶)
52, 3, 43eqtr4g 2798 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  ran crn 5677  cres 5678  cima 5679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689
This theorem is referenced by:  imaeq1i  6055  imaeq1d  6057  suppval  8145  naddcllem  8672  eceq2  8740  marypha1lem  9425  marypha1  9426  ackbij2lem2  10232  ackbij2lem3  10233  r1om  10236  limsupval  15415  isacs1i  17598  mreacs  17599  islindf  21359  iscnp  22733  xkoccn  23115  xkohaus  23149  xkoco1cn  23153  xkoco2cn  23154  xkococnlem  23155  xkococn  23156  xkoinjcn  23183  fmval  23439  fmf  23441  utoptop  23731  restutop  23734  restutopopn  23735  ustuqtoplem  23736  ustuqtop1  23738  ustuqtop2  23739  ustuqtop4  23741  ustuqtop5  23742  utopsnneiplem  23744  utopsnnei  23746  neipcfilu  23793  psmetutop  24068  cfilfval  24773  elply2  25702  coeeu  25731  coelem  25732  coeeq  25733  dmarea  26452  negsval  27490  mclsax  34549  tailfval  35246  bj-cleq  35832  bj-funun  36122  poimirlem15  36492  poimirlem24  36501  brtrclfv2  42464  liminfval  44462  isomgreqve  46480  isomgrsym  46491  isomgrtr  46494  ushrisomgr  46496
  Copyright terms: Public domain W3C validator