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

Theorem imaeq2d 5607
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 5603 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  cima 5252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-xp 5255  df-cnv 5257  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262
This theorem is referenced by:  imaeq12d  5608  nfimad  5616  csbima12  5624  elimasng  5632  elimasni  5633  inisegn0  5638  csbrn  5737  ressn  5815  foima  6261  f1imacnv  6294  dffv3  6328  fvco2  6415  fimacnvinrn2  6492  fsn2  6546  funfvima3  6638  isofrlem  6733  isoselem  6734  fnexALT  7279  curry1  7420  curry2  7423  fparlem3  7430  fparlem4  7431  suppsnop  7460  ressuppssdif  7467  imacosupp  7487  eceq1  7934  uniqs2  7961  ecinxp  7974  mapsnd  8051  sbthlem2  8227  sbth  8236  phplem4  8298  php3  8302  marypha1lem  8495  cantnfp1lem3  8741  tcrank  8911  fin4en1  9333  fin1a2lem7  9430  hsmexlem4  9453  hsmexlem5  9454  fpwwe2cbv  9654  fpwwe2lem3  9657  fpwwe2lem13  9666  fpwwecbv  9668  canth4  9671  frnnn0fsupp  11552  resunimafz0  13431  limsupgval  14415  isercoll  14606  vdwlem1  15892  vdwlem6  15897  vdwlem7  15898  vdwlem8  15899  vdwlem12  15903  vdwlem13  15904  vdwnn  15909  0ram  15931  ramz2  15935  isacs1i  16525  acsficl  17379  gsumvalx  17478  gsumpropd  17480  gsumpropd2lem  17481  gsumress  17484  efgrelexlema  18369  gsumval3a  18511  gsumval3lem1  18513  gsum2dlem2  18577  gsum2d2  18580  dprddisj  18616  dprdf1o  18639  dprdsn  18643  dprd2dlem2  18647  dprd2dlem1  18648  dprd2da  18649  dprd2db  18650  dmdprdsplit2lem  18652  dpjfval  18662  coe1mul2lem2  19853  frlmup3  20356  islindf  20368  islindf2  20370  lindfind  20372  f1lindf  20378  lmimlbs  20392  subbascn  21279  cncls2  21298  cncls  21299  cnntr  21300  cnpresti  21313  cnprest  21314  cnt1  21375  cnhaus  21379  cncmp  21416  cnconn  21446  1stcfb  21469  xkoccn  21643  ptrescn  21663  xkococnlem  21683  qtopeu  21740  qtoprest  21741  kqdisj  21756  kqcldsat  21757  ordthmeolem  21825  fmfnfmlem4  21981  ustuqtoplem  22263  utopsnneiplem  22271  utopsnneip  22272  ucncn  22309  metustto  22578  metustexhalf  22581  metustfbas  22582  cfilucfil  22584  metuust  22585  cfilucfil2  22586  metuel  22589  metuel2  22590  psmetutop  22592  restmetu  22595  metucn  22596  pi1addval  23067  iscph  23189  uniioombllem3  23573  dyadmbl  23588  mbfima  23618  mbfimaicc  23619  mbfimasn  23620  ismbfd  23627  ismbf2d  23628  ismbf3d  23641  mbfimaopnlem  23642  i1fd  23668  i1f1  23677  itg11  23678  i1faddlem  23680  i1fmullem  23681  i1fadd  23682  itg1addlem3  23685  itg1mulc  23691  itg2gt0  23747  limcnlp  23862  ellimc3  23863  limcflf  23865  limciun  23878  mdegval  24043  mdeg0  24050  mdegvsca  24056  mdegpropd  24064  deg1val  24076  ig1pval  24152  coeeu  24201  coeeq  24203  pserulm  24396  areambl  24906  pthdlem2  26899  eupth2lem3  27416  eupth2  27419  issh  28405  isch  28419  shsval  28511  sspreima  29787  dfcnv2  29816  gsummpt2co  30120  smatrcl  30202  locfinreflem  30247  zrhunitpreima  30362  mbfmco2  30667  sibfima  30740  sibfof  30742  eulerpartlemgv  30775  eulerpartlemn  30783  eulerpart  30784  orvcval4  30862  orvcelval  30870  orvcelel  30871  ballotlemscr  30920  erdszelem3  31513  erdsze  31522  cvmliftlem3  31607  cvmliftlem7  31611  cvmlift2lem9a  31623  msrval  31773  mvtinf  31790  mclsval  31798  mclsax  31804  mthmpps  31817  opelco3  32014  scutval  32248  madeval  32272  funpartlem  32386  tailval  32705  csbpredg  33509  ptrest  33741  poimirlem1  33743  poimirlem2  33744  poimirlem3  33745  poimirlem4  33746  poimirlem5  33747  poimirlem6  33748  poimirlem7  33749  poimirlem9  33751  poimirlem10  33752  poimirlem11  33753  poimirlem12  33754  poimirlem13  33755  poimirlem14  33756  poimirlem15  33757  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem22  33764  poimirlem23  33765  poimirlem24  33766  poimirlem25  33767  poimirlem26  33768  poimirlem27  33769  poimirlem28  33770  poimirlem29  33771  poimirlem31  33773  poimirlem32  33774  mblfinlem2  33780  volsupnfl  33787  itg2addnclem2  33794  sstotbnd2  33905  ismtyhmeolem  33935  grpokerinj  34024  lkrfval  34896  dnnumch3lem  38142  aomclem8  38157  pwfi2f1o  38192  cytpval  38313  frege97d  38570  frege109d  38575  frege131d  38582  nzprmdif  39044  wessf1ornlem  39891  limsuplesup  40449  limsupvaluz  40458  limsuplt2  40503  limsupge  40511  liminfgval  40512  liminfval2  40518  liminflelimsuplem  40525  liminflelimsup  40526  preimaioomnf  41449  imarnf1pr  41824
  Copyright terms: Public domain W3C validator