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

Theorem imaeq2i 5462
Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
Hypothesis
Ref Expression
imaeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
imaeq2i (𝐶𝐴) = (𝐶𝐵)

Proof of Theorem imaeq2i
StepHypRef Expression
1 imaeq1i.1 . 2 𝐴 = 𝐵
2 imaeq2 5460 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1482  cima 5115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-br 4652  df-opab 4711  df-xp 5118  df-cnv 5120  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125
This theorem is referenced by:  cnvimarndm  5484  dmco  5641  imain  5972  fnimapr  6260  ssimaex  6261  intpreima  6344  resfunexg  6476  imauni  6501  isoini2  6586  frnsuppeq  7304  imacosupp  7332  uniqs  7804  fiint  8234  jech9.3  8674  infxpenlem  8833  hsmexlem4  9248  frnnn0supp  11346  hashkf  13114  ghmeqker  17681  gsumval3lem1  18300  gsumval3lem2  18301  islinds2  20146  lindsind2  20152  snclseqg  21913  retopbas  22558  ismbf3d  23415  i1fima  23439  i1fd  23442  itg1addlem5  23461  limciun  23652  plyeq0  23961  spthispth  26616  0pth  26979  1pthdlem2  26989  eupth2lemb  27090  htth  27759  fcoinver  29402  ffs2  29488  ffsrn  29489  sibfof  30387  eulerpartgbij  30419  eulerpartlemmf  30422  eulerpartlemgh  30425  eulerpart  30429  fiblem  30445  orrvcval4  30511  cvmsss2  31241  opelco3  31662  madeval2  31920  poimirlem3  33392  poimirlem30  33419  mbfposadd  33437  itg2addnclem2  33442  ftc1anclem5  33469  ftc1anclem6  33470  pwfi2f1o  37492  brtrclfv2  37845  binomcxp  38382
  Copyright terms: Public domain W3C validator