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

Theorem imaeq2d 5157
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 5153 . 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 1362   "cima 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-xp 4833  df-cnv 4835  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840
This theorem is referenced by:  imaeq12d  5158  nfimad  5166  csbima12  5174  elimasng  5183  elimasni  5184  csbrn  5287  ressn  5361  foima  5613  f1imacnv  5645  dffv3  5675  fvco2  5754  fsn2  5870  funfvima3  5941  isofrlem  6018  isoselem  6019  fnexALT  6532  curry1  6653  curry2  6656  fparlem3  6663  fparlem4  6664  suppsnop  6693  ressuppssdif  6699  imacosupp  6718  eceq1  7125  uniqs2  7150  ecinxp  7163  mapsn  7242  sbthlem2  7410  sbth  7419  phplem4  7481  php3  7485  marypha1lem  7671  cantnffvalOLD  7859  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  wemapweOLD  7917  oef1oOLD  7919  tcrank  8079  fin4en1  8466  fin1a2lem7  8563  hsmexlem4  8586  hsmexlem5  8587  fpwwe2cbv  8785  fpwwe2lem3  8788  fpwwe2lem13  8797  fpwwecbv  8799  canth4  8802  frnnn0fsupp  10623  limsupgval  12938  isercoll  13129  vdwlem1  14025  vdwlem6  14030  vdwlem7  14031  vdwlem8  14032  vdwlem12  14036  vdwlem13  14037  vdwnn  14042  0ram  14064  ramz2  14068  isacs1i  14578  acsficl  15324  gsumvalx  15484  gsumpropd  15486  gsumress  15487  efgrelexlema  16226  gsumval3a  16359  gsumval3aOLD  16360  gsumval3lem1  16363  gsumzsubmclOLD  16383  gsum2dlem2  16436  gsum2dOLD  16438  gsum2d2  16440  pwsgsumOLD  16448  dprdvalOLD  16461  dprddisj  16467  dprdf1o  16503  dprdsn  16507  dprd2dlem2  16513  dprd2dlem1  16514  dprd2da  16515  dprd2db  16516  dmdprdsplit2lem  16518  dpjfval  16528  coe1mul2lem2  17620  frlmgsumOLD  18037  frlmup3  18070  islindf  18083  islindf2  18085  lindfind  18087  f1lindf  18093  lmimlbs  18107  subbascn  18700  cncls2  18719  cncls  18720  cnntr  18721  cnpresti  18734  cnprest  18735  cnt1  18796  cnhaus  18800  cncmp  18837  cnconn  18868  1stcfb  18891  xkoccn  19034  ptrescn  19054  xkococnlem  19074  qtopeu  19131  qtoprest  19132  kqdisj  19147  kqcldsat  19148  ordthmeolem  19216  fmfnfmlem4  19372  ustuqtoplem  19656  utopsnneiplem  19664  utopsnneip  19665  ucncn  19702  metusttoOLD  19974  metustto  19975  metustexhalfOLD  19980  metustexhalf  19981  metustfbasOLD  19982  metustfbas  19983  cfilucfilOLD  19986  cfilucfil  19987  metuustOLD  19988  metuust  19989  cfilucfil2OLD  19990  cfilucfil2  19991  metuelOLD  19994  metuel  19995  metuel2  19996  metutopOLD  19999  psmetutop  20000  restmetu  20004  metucnOLD  20005  metucn  20006  pi1addval  20462  iscph  20531  uniioombllem3  20907  dyadmbl  20922  mbfima  20952  mbfimaicc  20953  mbfimasn  20954  ismbfd  20960  ismbf2d  20961  ismbf3d  20974  mbfimaopnlem  20975  i1fd  21001  i1f1  21010  itg11  21011  i1faddlem  21013  i1fmullem  21014  i1fadd  21015  itg1addlem3  21018  itg1mulc  21024  itg2gt0  21080  limcnlp  21195  ellimc3  21196  limcflf  21198  limciun  21211  mdegfvalOLD  21417  mdegval  21418  mdegvalOLD  21419  mdeg0  21426  mdegvsca  21432  mdegpropd  21440  deg1val  21452  ig1pval  21529  coeeu  21578  coeeq  21580  pserulm  21772  areambl  22237  spthispth  23295  1pthonlem2  23312  constr2pth  23323  constr3pthlem3  23366  eupath2lem3  23423  eupath2  23424  efghgrp  23683  issh  24433  isch  24448  shsval  24538  fimacnvinrn2  25777  sspreima  25786  dfcnv2  25818  gsumpropd2lem  26093  zrhunitpreima  26261  mbfmco2  26534  sibfima  26572  sibfof  26574  eulerpartlemgv  26604  eulerpartlemn  26612  eulerpart  26613  orvcval4  26691  orvcelval  26699  orvcelel  26700  ballotlemscr  26749  erdszelem3  26929  erdsze  26938  cvmliftlem3  27024  cvmliftlem7  27028  cvmlift2lem9a  27040  opelco3  27436  nofulllem1  27690  nofulllem2  27691  funpartlem  27820  ptrest  28269  mblfinlem2  28273  volsupnfl  28280  itg2addnclem2  28288  tailval  28438  sstotbnd2  28517  ismtyhmeolem  28547  grpokerinj  28594  inisegn0  29241  dnnumch3lem  29244  aomclem8  29259  mapfien2OLD  29294  pwfi2f1o  29296  cytpval  29422  imarnf1pr  29996  usgra2pthspth  30141  usgra2adedglem1  30154  csbfv12gALTOLD  31259  lkrfval  32305
  Copyright terms: Public domain W3C validator