Theorem imaeq2d 5385

Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Hypothesis

Ref	Expression
imaeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
imaeq2d	⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Proof of Theorem imaeq2d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		imaeq2 5381	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1475   “ cima 5041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  imaeq12d  5386  nfimad  5394  csbima12  5402  elimasng  5410  elimasni  5411  inisegn0  5416  csbrn  5514  ressn  5588  foima  6033  f1imacnv  6066  dffv3  6099  fvco2  6183  fimacnvinrn2  6257  fsn2  6309  funfvima3  6399  isofrlem  6490  isoselem  6491  fnexALT  7025  curry1  7156  curry2  7159  fparlem3  7166  fparlem4  7167  suppsnop  7196  ressuppssdif  7203  imacosupp  7222  eceq1  7669  uniqs2  7696  ecinxp  7709  mapsn  7785  sbthlem2  7956  sbth  7965  phplem4  8027  php3  8031  marypha1lem  8222  cantnfp1lem3  8460  tcrank  8630  fin4en1  9014  fin1a2lem7  9111  hsmexlem4  9134  hsmexlem5  9135  fpwwe2cbv  9331  fpwwe2lem3  9334  fpwwe2lem13  9343  fpwwecbv  9345  canth4  9348  frnnn0fsupp  11227  limsupgval  14055  isercoll  14246  vdwlem1  15523  vdwlem6  15528  vdwlem7  15529  vdwlem8  15530  vdwlem12  15534  vdwlem13  15535  vdwnn  15540  0ram  15562  ramz2  15566  isacs1i  16141  acsficl  16994  gsumvalx  17093  gsumpropd  17095  gsumpropd2lem  17096  gsumress  17099  efgrelexlema  17985  gsumval3a  18127  gsumval3lem1  18129  gsum2dlem2  18193  gsum2d2  18196  dprddisj  18231  dprdf1o  18254  dprdsn  18258  dprd2dlem2  18262  dprd2dlem1  18263  dprd2da  18264  dprd2db  18265  dmdprdsplit2lem  18267  dpjfval  18277  coe1mul2lem2  19459  frlmup3  19958  islindf  19970  islindf2  19972  lindfind  19974  f1lindf  19980  lmimlbs  19994  subbascn  20868  cncls2  20887  cncls  20888  cnntr  20889  cnpresti  20902  cnprest  20903  cnt1  20964  cnhaus  20968  cncmp  21005  cnconn  21035  1stcfb  21058  xkoccn  21232  ptrescn  21252  xkococnlem  21272  qtopeu  21329  qtoprest  21330  kqdisj  21345  kqcldsat  21346  ordthmeolem  21414  fmfnfmlem4  21571  ustuqtoplem  21853  utopsnneiplem  21861  utopsnneip  21862  ucncn  21899  metustto  22168  metustexhalf  22171  metustfbas  22172  cfilucfil  22174  metuust  22175  cfilucfil2  22176  metuel  22179  metuel2  22180  psmetutop  22182  restmetu  22185  metucn  22186  pi1addval  22656  iscph  22778  uniioombllem3  23159  dyadmbl  23174  mbfima  23205  mbfimaicc  23206  mbfimasn  23207  ismbfd  23213  ismbf2d  23214  ismbf3d  23227  mbfimaopnlem  23228  i1fd  23254  i1f1  23263  itg11  23264  i1faddlem  23266  i1fmullem  23267  i1fadd  23268  itg1addlem3  23271  itg1mulc  23277  itg2gt0  23333  limcnlp  23448  ellimc3  23449  limcflf  23451  limciun  23464  mdegval  23627  mdeg0  23634  mdegvsca  23640  mdegpropd  23648  deg1val  23660  ig1pval  23736  coeeu  23785  coeeq  23787  pserulm  23980  areambl  24485  spthispth  26103  1pthonlem2  26120  constr2pth  26131  constr3pthlem3  26185  eupath2lem3  26506  eupath2  26507  issh  27449  isch  27463  shsval  27555  sspreima  28827  dfcnv2  28859  gsummpt2co  29111  smatrcl  29190  locfinreflem  29235  zrhunitpreima  29350  mbfmco2  29654  sibfima  29727  sibfof  29729  eulerpartlemgv  29762  eulerpartlemn  29770  eulerpart  29771  orvcval4  29849  orvcelval  29857  orvcelel  29858  ballotlemscr  29907  erdszelem3  30429  erdsze  30438  cvmliftlem3  30523  cvmliftlem7  30527  cvmlift2lem9a  30539  msrval  30689  mvtinf  30706  mclsval  30714  mclsax  30720  mthmpps  30733  opelco3  30923  nofulllem1  31101  nofulllem2  31102  funpartlem  31219  tailval  31538  csbpredg  32348  ptrest  32578  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem29  32608  poimirlem31  32610  poimirlem32  32611  mblfinlem2  32617  volsupnfl  32624  itg2addnclem2  32632  sstotbnd2  32743  ismtyhmeolem  32773  grpokerinj  32862  lkrfval  33392  dnnumch3lem  36634  aomclem8  36649  pwfi2f1o  36684  cytpval  36806  frege97d  37063  frege109d  37068  frege131d  37075  nzprmdif  37540  csbfv12gALTOLD  38074  wessf1ornlem  38366  mapsnd  38383  preimaioomnf  39606  imarnf1pr  40326  resunimafz0  40368  pthdlem2  40974  eupth2lem3  41404  eupth2  41407