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 2495 1  |-  ( ph  ->  ( A " C
)  =  ( B
" D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   "cima 4952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402  df-opab 4460  df-xp 4955  df-cnv 4957  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962
This theorem is referenced by:  csbima12  5295  csbima12gOLD  5296  vdwpc  14160  dmdprd  16603  isunit  16873  qtopval  19401  limciun  21503  ig1pval  21778  ispth  23620  qqhval  26549  eulerpartgbij  26900  orvcval  26985  ballotlemrval  27045  ballotlemrinv0  27060  ballotlemrinv  27061  predeq123  27771  itg2addnclem2  28593  islmodfg  29571  bj-projeq  32818
  Copyright terms: Public domain W3C validator