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

Theorem imaeq2d 5616
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 5612 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  cima 5261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4797  df-opab 4857  df-xp 5264  df-cnv 5266  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271
This theorem is referenced by:  imaeq12d  5617  nfimad  5625  csbima12  5633  elimasng  5641  elimasni  5642  inisegn0  5647  csbrn  5746  ressn  5824  foima  6273  f1imacnv  6306  dffv3  6340  fvco2  6427  fimacnvinrn2  6504  fsn2  6558  funfvima3  6650  isofrlem  6745  isoselem  6746  fnexALT  7289  curry1  7429  curry2  7432  fparlem3  7439  fparlem4  7440  suppsnop  7469  ressuppssdif  7476  imacosupp  7496  eceq1  7941  uniqs2  7968  ecinxp  7981  mapsn  8057  sbthlem2  8228  sbth  8237  phplem4  8299  php3  8303  marypha1lem  8496  cantnfp1lem3  8742  tcrank  8912  fin4en1  9315  fin1a2lem7  9412  hsmexlem4  9435  hsmexlem5  9436  fpwwe2cbv  9636  fpwwe2lem3  9639  fpwwe2lem13  9648  fpwwecbv  9650  canth4  9653  frnnn0fsupp  11534  resunimafz0  13413  limsupgval  14398  isercoll  14589  vdwlem1  15879  vdwlem6  15884  vdwlem7  15885  vdwlem8  15886  vdwlem12  15890  vdwlem13  15891  vdwnn  15896  0ram  15918  ramz2  15922  isacs1i  16511  acsficl  17364  gsumvalx  17463  gsumpropd  17465  gsumpropd2lem  17466  gsumress  17469  efgrelexlema  18354  gsumval3a  18496  gsumval3lem1  18498  gsum2dlem2  18562  gsum2d2  18565  dprddisj  18600  dprdf1o  18623  dprdsn  18627  dprd2dlem2  18631  dprd2dlem1  18632  dprd2da  18633  dprd2db  18634  dmdprdsplit2lem  18636  dpjfval  18646  coe1mul2lem2  19832  frlmup3  20333  islindf  20345  islindf2  20347  lindfind  20349  f1lindf  20355  lmimlbs  20369  subbascn  21252  cncls2  21271  cncls  21272  cnntr  21273  cnpresti  21286  cnprest  21287  cnt1  21348  cnhaus  21352  cncmp  21389  cnconn  21419  1stcfb  21442  xkoccn  21616  ptrescn  21636  xkococnlem  21656  qtopeu  21713  qtoprest  21714  kqdisj  21729  kqcldsat  21730  ordthmeolem  21798  fmfnfmlem4  21954  ustuqtoplem  22236  utopsnneiplem  22244  utopsnneip  22245  ucncn  22282  metustto  22551  metustexhalf  22554  metustfbas  22555  cfilucfil  22557  metuust  22558  cfilucfil2  22559  metuel  22562  metuel2  22563  psmetutop  22565  restmetu  22568  metucn  22569  pi1addval  23040  iscph  23162  uniioombllem3  23545  dyadmbl  23560  mbfima  23590  mbfimaicc  23591  mbfimasn  23592  ismbfd  23598  ismbf2d  23599  ismbf3d  23612  mbfimaopnlem  23613  i1fd  23639  i1f1  23648  itg11  23649  i1faddlem  23651  i1fmullem  23652  i1fadd  23653  itg1addlem3  23656  itg1mulc  23662  itg2gt0  23718  limcnlp  23833  ellimc3  23834  limcflf  23836  limciun  23849  mdegval  24014  mdeg0  24021  mdegvsca  24027  mdegpropd  24035  deg1val  24047  ig1pval  24123  coeeu  24172  coeeq  24174  pserulm  24367  areambl  24876  pthdlem2  26866  eupth2lem3  27380  eupth2  27383  issh  28366  isch  28380  shsval  28472  sspreima  29748  dfcnv2  29777  gsummpt2co  30081  smatrcl  30163  locfinreflem  30208  zrhunitpreima  30323  mbfmco2  30628  sibfima  30701  sibfof  30703  eulerpartlemgv  30736  eulerpartlemn  30744  eulerpart  30745  orvcval4  30823  orvcelval  30831  orvcelel  30832  ballotlemscr  30881  erdszelem3  31474  erdsze  31483  cvmliftlem3  31568  cvmliftlem7  31572  cvmlift2lem9a  31584  msrval  31734  mvtinf  31751  mclsval  31759  mclsax  31765  mthmpps  31778  opelco3  31975  scutval  32209  madeval  32233  funpartlem  32347  tailval  32666  csbpredg  33475  ptrest  33713  poimirlem1  33715  poimirlem2  33716  poimirlem3  33717  poimirlem4  33718  poimirlem5  33719  poimirlem6  33720  poimirlem7  33721  poimirlem9  33723  poimirlem10  33724  poimirlem11  33725  poimirlem12  33726  poimirlem13  33727  poimirlem14  33728  poimirlem15  33729  poimirlem16  33730  poimirlem17  33731  poimirlem19  33733  poimirlem20  33734  poimirlem22  33736  poimirlem23  33737  poimirlem24  33738  poimirlem25  33739  poimirlem26  33740  poimirlem27  33741  poimirlem28  33742  poimirlem29  33743  poimirlem31  33745  poimirlem32  33746  mblfinlem2  33752  volsupnfl  33759  itg2addnclem2  33767  sstotbnd2  33878  ismtyhmeolem  33908  grpokerinj  33997  lkrfval  34869  dnnumch3lem  38110  aomclem8  38125  pwfi2f1o  38160  cytpval  38281  frege97d  38538  frege109d  38543  frege131d  38550  nzprmdif  39012  wessf1ornlem  39862  mapsnd  39879  limsuplesup  40426  limsupvaluz  40435  limsuplt2  40480  limsupge  40488  liminfgval  40489  liminfval2  40495  liminflelimsuplem  40502  liminflelimsup  40503  preimaioomnf  41427  imarnf1pr  41801
  Copyright terms: Public domain W3C validator