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

Theorem imaeq2d 5435
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 5431 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cima 5087
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 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-xp 5090  df-cnv 5092  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097
This theorem is referenced by:  imaeq12d  5436  nfimad  5444  csbima12  5452  elimasng  5460  elimasni  5461  inisegn0  5466  csbrn  5565  ressn  5640  foima  6087  f1imacnv  6120  dffv3  6154  fvco2  6240  fimacnvinrn2  6315  fsn2  6368  funfvima3  6460  isofrlem  6555  isoselem  6556  fnexALT  7094  curry1  7229  curry2  7232  fparlem3  7239  fparlem4  7240  suppsnop  7269  ressuppssdif  7276  imacosupp  7295  eceq1  7742  uniqs2  7769  ecinxp  7782  mapsn  7859  sbthlem2  8031  sbth  8040  phplem4  8102  php3  8106  marypha1lem  8299  cantnfp1lem3  8537  tcrank  8707  fin4en1  9091  fin1a2lem7  9188  hsmexlem4  9211  hsmexlem5  9212  fpwwe2cbv  9412  fpwwe2lem3  9415  fpwwe2lem13  9424  fpwwecbv  9426  canth4  9429  frnnn0fsupp  11310  resunimafz0  13183  limsupgval  14157  isercoll  14348  vdwlem1  15628  vdwlem6  15633  vdwlem7  15634  vdwlem8  15635  vdwlem12  15639  vdwlem13  15640  vdwnn  15645  0ram  15667  ramz2  15671  isacs1i  16258  acsficl  17111  gsumvalx  17210  gsumpropd  17212  gsumpropd2lem  17213  gsumress  17216  efgrelexlema  18102  gsumval3a  18244  gsumval3lem1  18246  gsum2dlem2  18310  gsum2d2  18313  dprddisj  18348  dprdf1o  18371  dprdsn  18375  dprd2dlem2  18379  dprd2dlem1  18380  dprd2da  18381  dprd2db  18382  dmdprdsplit2lem  18384  dpjfval  18394  coe1mul2lem2  19578  frlmup3  20079  islindf  20091  islindf2  20093  lindfind  20095  f1lindf  20101  lmimlbs  20115  subbascn  20998  cncls2  21017  cncls  21018  cnntr  21019  cnpresti  21032  cnprest  21033  cnt1  21094  cnhaus  21098  cncmp  21135  cnconn  21165  1stcfb  21188  xkoccn  21362  ptrescn  21382  xkococnlem  21402  qtopeu  21459  qtoprest  21460  kqdisj  21475  kqcldsat  21476  ordthmeolem  21544  fmfnfmlem4  21701  ustuqtoplem  21983  utopsnneiplem  21991  utopsnneip  21992  ucncn  22029  metustto  22298  metustexhalf  22301  metustfbas  22302  cfilucfil  22304  metuust  22305  cfilucfil2  22306  metuel  22309  metuel2  22310  psmetutop  22312  restmetu  22315  metucn  22316  pi1addval  22788  iscph  22910  uniioombllem3  23293  dyadmbl  23308  mbfima  23339  mbfimaicc  23340  mbfimasn  23341  ismbfd  23347  ismbf2d  23348  ismbf3d  23361  mbfimaopnlem  23362  i1fd  23388  i1f1  23397  itg11  23398  i1faddlem  23400  i1fmullem  23401  i1fadd  23402  itg1addlem3  23405  itg1mulc  23411  itg2gt0  23467  limcnlp  23582  ellimc3  23583  limcflf  23585  limciun  23598  mdegval  23761  mdeg0  23768  mdegvsca  23774  mdegpropd  23782  deg1val  23794  ig1pval  23870  coeeu  23919  coeeq  23921  pserulm  24114  areambl  24619  pthdlem2  26567  eupth2lem3  26996  eupth2  26999  issh  27953  isch  27967  shsval  28059  sspreima  29330  dfcnv2  29360  gsummpt2co  29607  smatrcl  29686  locfinreflem  29731  zrhunitpreima  29846  mbfmco2  30150  sibfima  30223  sibfof  30225  eulerpartlemgv  30258  eulerpartlemn  30266  eulerpart  30267  orvcval4  30345  orvcelval  30353  orvcelel  30354  ballotlemscr  30403  erdszelem3  30936  erdsze  30945  cvmliftlem3  31030  cvmliftlem7  31034  cvmlift2lem9a  31046  msrval  31196  mvtinf  31213  mclsval  31221  mclsax  31227  mthmpps  31240  opelco3  31433  funpartlem  31744  tailval  32063  csbpredg  32843  ptrest  33079  poimirlem1  33081  poimirlem2  33082  poimirlem3  33083  poimirlem4  33084  poimirlem5  33085  poimirlem6  33086  poimirlem7  33087  poimirlem9  33089  poimirlem10  33090  poimirlem11  33091  poimirlem12  33092  poimirlem13  33093  poimirlem14  33094  poimirlem15  33095  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  poimirlem22  33102  poimirlem23  33103  poimirlem24  33104  poimirlem25  33105  poimirlem26  33106  poimirlem27  33107  poimirlem28  33108  poimirlem29  33109  poimirlem31  33111  poimirlem32  33112  mblfinlem2  33118  volsupnfl  33125  itg2addnclem2  33133  sstotbnd2  33244  ismtyhmeolem  33274  grpokerinj  33363  lkrfval  33893  dnnumch3lem  37135  aomclem8  37150  pwfi2f1o  37185  cytpval  37307  frege97d  37564  frege109d  37569  frege131d  37576  nzprmdif  38039  csbfv12gALTOLD  38574  wessf1ornlem  38880  mapsnd  38897  limsuplesup  39367  limsupvaluz  39376  preimaioomnf  40266  imarnf1pr  40628
  Copyright terms: Public domain W3C validator