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

Theorem imaeq2d 5276
Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
Hypothesis
Ref Expression
imaeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
imaeq2d  |-  ( ph  ->  ( C " A
)  =  ( C
" B ) )

Proof of Theorem imaeq2d
StepHypRef Expression
1 imaeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 imaeq2 5272 . 2  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
31, 2syl 16 1  |-  ( ph  ->  ( C " A
)  =  ( C
" B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   "cima 4950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-xp 4953  df-cnv 4955  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960
This theorem is referenced by:  imaeq12d  5277  nfimad  5285  csbima12  5293  elimasng  5302  elimasni  5303  csbrn  5406  ressn  5480  foima  5732  f1imacnv  5764  dffv3  5794  fvco2  5874  fsn2  5991  funfvima3  6062  isofrlem  6139  isoselem  6140  fnexALT  6652  curry1  6773  curry2  6776  fparlem3  6783  fparlem4  6784  suppsnop  6813  ressuppssdif  6819  imacosupp  6838  eceq1  7246  uniqs2  7271  ecinxp  7284  mapsn  7363  sbthlem2  7531  sbth  7540  phplem4  7602  php3  7606  marypha1lem  7793  cantnffvalOLD  7981  cantnfp1lem3  7998  cantnfp1lem3OLD  8024  wemapweOLD  8039  oef1oOLD  8041  tcrank  8201  fin4en1  8588  fin1a2lem7  8685  hsmexlem4  8708  hsmexlem5  8709  fpwwe2cbv  8907  fpwwe2lem3  8910  fpwwe2lem13  8919  fpwwecbv  8921  canth4  8924  frnnn0fsupp  10745  limsupgval  13071  isercoll  13262  vdwlem1  14159  vdwlem6  14164  vdwlem7  14165  vdwlem8  14166  vdwlem12  14170  vdwlem13  14171  vdwnn  14176  0ram  14198  ramz2  14202  isacs1i  14713  acsficl  15459  gsumvalx  15620  gsumpropd  15622  gsumpropd2lem  15623  gsumress  15625  efgrelexlema  16366  gsumval3a  16499  gsumval3aOLD  16500  gsumval3lem1  16503  gsumzsubmclOLD  16523  gsum2dlem2  16583  gsum2dOLD  16585  gsum2d2  16587  pwsgsumOLD  16595  dprdvalOLD  16608  dprddisj  16614  dprdf1o  16650  dprdsn  16654  dprd2dlem2  16660  dprd2dlem1  16661  dprd2da  16662  dprd2db  16663  dmdprdsplit2lem  16665  dpjfval  16675  coe1mul2lem2  17844  frlmgsumOLD  18319  frlmup3  18352  islindf  18365  islindf2  18367  lindfind  18369  f1lindf  18375  lmimlbs  18389  subbascn  18989  cncls2  19008  cncls  19009  cnntr  19010  cnpresti  19023  cnprest  19024  cnt1  19085  cnhaus  19089  cncmp  19126  cnconn  19157  1stcfb  19180  xkoccn  19323  ptrescn  19343  xkococnlem  19363  qtopeu  19420  qtoprest  19421  kqdisj  19436  kqcldsat  19437  ordthmeolem  19505  fmfnfmlem4  19661  ustuqtoplem  19945  utopsnneiplem  19953  utopsnneip  19954  ucncn  19991  metusttoOLD  20263  metustto  20264  metustexhalfOLD  20269  metustexhalf  20270  metustfbasOLD  20271  metustfbas  20272  cfilucfilOLD  20275  cfilucfil  20276  metuustOLD  20277  metuust  20278  cfilucfil2OLD  20279  cfilucfil2  20280  metuelOLD  20283  metuel  20284  metuel2  20285  metutopOLD  20288  psmetutop  20289  restmetu  20293  metucnOLD  20294  metucn  20295  pi1addval  20751  iscph  20820  uniioombllem3  21197  dyadmbl  21212  mbfima  21242  mbfimaicc  21243  mbfimasn  21244  ismbfd  21250  ismbf2d  21251  ismbf3d  21264  mbfimaopnlem  21265  i1fd  21291  i1f1  21300  itg11  21301  i1faddlem  21303  i1fmullem  21304  i1fadd  21305  itg1addlem3  21308  itg1mulc  21314  itg2gt0  21370  limcnlp  21485  ellimc3  21486  limcflf  21488  limciun  21501  mdegfvalOLD  21664  mdegval  21665  mdegvalOLD  21666  mdeg0  21673  mdegvsca  21679  mdegpropd  21687  deg1val  21699  ig1pval  21776  coeeu  21825  coeeq  21827  pserulm  22019  areambl  22484  spthispth  23623  1pthonlem2  23640  constr2pth  23651  constr3pthlem3  23694  eupath2lem3  23751  eupath2  23752  efghgrp  24011  issh  24761  isch  24776  shsval  24866  fimacnvinrn2  26103  sspreima  26112  dfcnv2  26144  zrhunitpreima  26551  mbfmco2  26823  sibfima  26867  sibfof  26869  eulerpartlemgv  26899  eulerpartlemn  26907  eulerpart  26908  orvcval4  26986  orvcelval  26994  orvcelel  26995  ballotlemscr  27044  erdszelem3  27224  erdsze  27233  cvmliftlem3  27319  cvmliftlem7  27323  cvmlift2lem9a  27335  opelco3  27732  nofulllem1  27986  nofulllem2  27987  funpartlem  28116  ptrest  28572  mblfinlem2  28576  volsupnfl  28583  itg2addnclem2  28591  tailval  28741  sstotbnd2  28820  ismtyhmeolem  28850  grpokerinj  28897  inisegn0  29543  dnnumch3lem  29546  aomclem8  29561  mapfien2OLD  29596  pwfi2f1o  29598  cytpval  29724  imarnf1pr  30297  usgra2pthspth  30442  usgra2adedglem1  30455  csbfv12gALTOLD  31874  lkrfval  33055
  Copyright terms: Public domain W3C validator