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

Theorem imaeq12d 5279
Description: Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.)
Hypotheses
Ref Expression
imaeq1d.1  |-  ( ph  ->  A  =  B )
imaeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
imaeq12d  |-  ( ph  ->  ( A " C
)  =  ( B
" D ) )

Proof of Theorem imaeq12d
StepHypRef Expression
1 imaeq1d.1 . . 3  |-  ( ph  ->  A  =  B )
21imaeq1d 5277 . 2  |-  ( ph  ->  ( A " C
)  =  ( B
" C ) )
3 imaeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43imaeq2d 5278 . 2  |-  ( ph  ->  ( B " C
)  =  ( B
" D ) )
52, 4eqtrd 2443 1  |-  ( ph  ->  ( A " C
)  =  ( B
" D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405   "cima 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-xp 4948  df-cnv 4950  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955
This theorem is referenced by:  csbima12  5295  csbima12gOLD  5296  vdwpc  14599  dmdprd  17241  isunit  17518  qtopval  20380  limciun  22482  ig1pval  22757  ispth  24868  qqhval  28287  eulerpartgbij  28697  orvcval  28782  ballotlemrval  28842  ballotlemrinv0  28857  ballotlemrinv  28858  mthmval  29668  predeq123  29918  bj-projeq  31103  itg2addnclem2  31421  islmodfg  35358  heeq12  35737
  Copyright terms: Public domain W3C validator