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

Theorem imaeq2i 5452
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 5450 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  cima 5107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-cnv 5112  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117
This theorem is referenced by:  cnvimarndm  5474  dmco  5631  imain  5962  fnimapr  6249  ssimaex  6250  intpreima  6332  resfunexg  6464  imauni  6489  isoini2  6574  frnsuppeq  7292  imacosupp  7320  uniqs  7792  fiint  8222  jech9.3  8662  infxpenlem  8821  hsmexlem4  9236  frnnn0supp  11334  hashkf  13102  ghmeqker  17668  gsumval3lem1  18287  gsumval3lem2  18288  islinds2  20133  lindsind2  20139  snclseqg  21900  retopbas  22545  ismbf3d  23402  i1fima  23426  i1fd  23429  itg1addlem5  23448  limciun  23639  plyeq0  23948  spthispth  26603  0pth  26966  1pthdlem2  26976  eupth2lemb  27077  htth  27745  fcoinver  29390  ffs2  29477  ffsrn  29478  sibfof  30376  eulerpartgbij  30408  eulerpartlemmf  30411  eulerpartlemgh  30414  eulerpart  30418  fiblem  30434  orrvcval4  30500  cvmsss2  31230  opelco3  31652  madeval2  31910  poimirlem3  33383  poimirlem30  33410  mbfposadd  33428  itg2addnclem2  33433  ftc1anclem5  33460  ftc1anclem6  33461  pwfi2f1o  37485  brtrclfv2  37838  binomcxp  38376
  Copyright terms: Public domain W3C validator