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

Theorem imaeq1 5167
Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
imaeq1  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )

Proof of Theorem imaeq1
StepHypRef Expression
1 reseq1 5107 . . 3  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
21rneqd 5070 . 2  |-  ( A  =  B  ->  ran  ( A  |`  C )  =  ran  ( B  |`  C ) )
3 df-ima 4856 . 2  |-  ( A
" C )  =  ran  ( A  |`  C )
4 df-ima 4856 . 2  |-  ( B
" C )  =  ran  ( B  |`  C )
52, 3, 43eqtr4g 2500 1  |-  ( A  =  B  ->  ( A " C )  =  ( B " C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   ran crn 4844    |` cres 4845   "cima 4846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-br 4296  df-opab 4354  df-cnv 4851  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856
This theorem is referenced by:  imaeq1i  5169  imaeq1d  5171  suppval  6695  eceq2  7141  marypha1lem  7686  marypha1  7687  ackbij2lem2  8412  ackbij2lem3  8413  r1om  8416  limsupval  12955  isacs1i  14598  mreacs  14599  islindf  18244  iscnp  18844  xkoccn  19195  xkohaus  19229  xkoco1cn  19233  xkoco2cn  19234  xkococnlem  19235  xkococn  19236  xkoinjcn  19263  fmval  19519  fmf  19521  utoptop  19812  restutop  19815  restutopopn  19816  ustuqtoplem  19817  ustuqtop1  19819  ustuqtop2  19820  ustuqtop4  19822  ustuqtop5  19823  utopsnneiplem  19825  utopsnnei  19827  neipcfilu  19874  metutopOLD  20160  psmetutop  20161  cfilfval  20778  elply2  21667  coeeu  21696  coelem  21697  coeeq  21698  dmarea  22354  tailfval  28596  bj-cleq  32457
  Copyright terms: Public domain W3C validator