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

Theorem imaeq2d 5430
Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
Hypothesis
Ref Expression
imaeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
imaeq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem imaeq2d
StepHypRef Expression
1 imaeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 imaeq2 5426 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cima 5082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619  df-opab 4679  df-xp 5085  df-cnv 5087  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092
This theorem is referenced by:  imaeq12d  5431  nfimad  5439  csbima12  5447  elimasng  5455  elimasni  5456  inisegn0  5461  csbrn  5560  ressn  5635  foima  6082  f1imacnv  6115  dffv3  6149  fvco2  6235  fimacnvinrn2  6310  fsn2  6363  funfvima3  6455  isofrlem  6550  isoselem  6551  fnexALT  7086  curry1  7221  curry2  7224  fparlem3  7231  fparlem4  7232  suppsnop  7261  ressuppssdif  7268  imacosupp  7287  eceq1  7734  uniqs2  7761  ecinxp  7774  mapsn  7850  sbthlem2  8022  sbth  8031  phplem4  8093  php3  8097  marypha1lem  8290  cantnfp1lem3  8528  tcrank  8698  fin4en1  9082  fin1a2lem7  9179  hsmexlem4  9202  hsmexlem5  9203  fpwwe2cbv  9403  fpwwe2lem3  9406  fpwwe2lem13  9415  fpwwecbv  9417  canth4  9420  frnnn0fsupp  11301  resunimafz0  13174  limsupgval  14148  isercoll  14339  vdwlem1  15616  vdwlem6  15621  vdwlem7  15622  vdwlem8  15623  vdwlem12  15627  vdwlem13  15628  vdwnn  15633  0ram  15655  ramz2  15659  isacs1i  16246  acsficl  17099  gsumvalx  17198  gsumpropd  17200  gsumpropd2lem  17201  gsumress  17204  efgrelexlema  18090  gsumval3a  18232  gsumval3lem1  18234  gsum2dlem2  18298  gsum2d2  18301  dprddisj  18336  dprdf1o  18359  dprdsn  18363  dprd2dlem2  18367  dprd2dlem1  18368  dprd2da  18369  dprd2db  18370  dmdprdsplit2lem  18372  dpjfval  18382  coe1mul2lem2  19566  frlmup3  20067  islindf  20079  islindf2  20081  lindfind  20083  f1lindf  20089  lmimlbs  20103  subbascn  20977  cncls2  20996  cncls  20997  cnntr  20998  cnpresti  21011  cnprest  21012  cnt1  21073  cnhaus  21077  cncmp  21114  cnconn  21144  1stcfb  21167  xkoccn  21341  ptrescn  21361  xkococnlem  21381  qtopeu  21438  qtoprest  21439  kqdisj  21454  kqcldsat  21455  ordthmeolem  21523  fmfnfmlem4  21680  ustuqtoplem  21962  utopsnneiplem  21970  utopsnneip  21971  ucncn  22008  metustto  22277  metustexhalf  22280  metustfbas  22281  cfilucfil  22283  metuust  22284  cfilucfil2  22285  metuel  22288  metuel2  22289  psmetutop  22291  restmetu  22294  metucn  22295  pi1addval  22767  iscph  22889  uniioombllem3  23272  dyadmbl  23287  mbfima  23318  mbfimaicc  23319  mbfimasn  23320  ismbfd  23326  ismbf2d  23327  ismbf3d  23340  mbfimaopnlem  23341  i1fd  23367  i1f1  23376  itg11  23377  i1faddlem  23379  i1fmullem  23380  i1fadd  23381  itg1addlem3  23384  itg1mulc  23390  itg2gt0  23446  limcnlp  23561  ellimc3  23562  limcflf  23564  limciun  23577  mdegval  23740  mdeg0  23747  mdegvsca  23753  mdegpropd  23761  deg1val  23773  ig1pval  23849  coeeu  23898  coeeq  23900  pserulm  24093  areambl  24598  pthdlem2  26546  eupth2lem3  26975  eupth2  26978  issh  27932  isch  27946  shsval  28038  sspreima  29307  dfcnv2  29337  gsummpt2co  29583  smatrcl  29662  locfinreflem  29707  zrhunitpreima  29822  mbfmco2  30126  sibfima  30199  sibfof  30201  eulerpartlemgv  30234  eulerpartlemn  30242  eulerpart  30243  orvcval4  30321  orvcelval  30329  orvcelel  30330  ballotlemscr  30379  erdszelem3  30910  erdsze  30919  cvmliftlem3  31004  cvmliftlem7  31008  cvmlift2lem9a  31020  msrval  31170  mvtinf  31187  mclsval  31195  mclsax  31201  mthmpps  31214  opelco3  31407  funpartlem  31718  tailval  32037  csbpredg  32831  ptrest  33067  poimirlem1  33069  poimirlem2  33070  poimirlem3  33071  poimirlem4  33072  poimirlem5  33073  poimirlem6  33074  poimirlem7  33075  poimirlem9  33077  poimirlem10  33078  poimirlem11  33079  poimirlem12  33080  poimirlem13  33081  poimirlem14  33082  poimirlem15  33083  poimirlem16  33084  poimirlem17  33085  poimirlem19  33087  poimirlem20  33088  poimirlem22  33090  poimirlem23  33091  poimirlem24  33092  poimirlem25  33093  poimirlem26  33094  poimirlem27  33095  poimirlem28  33096  poimirlem29  33097  poimirlem31  33099  poimirlem32  33100  mblfinlem2  33106  volsupnfl  33113  itg2addnclem2  33121  sstotbnd2  33232  ismtyhmeolem  33262  grpokerinj  33351  lkrfval  33881  dnnumch3lem  37123  aomclem8  37138  pwfi2f1o  37173  cytpval  37295  frege97d  37552  frege109d  37557  frege131d  37564  nzprmdif  38027  csbfv12gALTOLD  38562  wessf1ornlem  38868  mapsnd  38885  limsuplesup  39358  limsupvaluz  39367  preimaioomnf  40257  imarnf1pr  40619
  Copyright terms: Public domain W3C validator