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

Theorem mpteq12 4485
Description: An equality theorem for the maps to notation. (Contributed by NM, 16-Dec-2013.)
Assertion
Ref Expression
mpteq12  |-  ( ( A  =  C  /\  A. x  e.  A  B  =  D )  ->  (
x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Distinct variable groups:    x, A    x, C
Allowed substitution hints:    B( x)    D( x)

Proof of Theorem mpteq12
StepHypRef Expression
1 ax-5 1760 . 2  |-  ( A  =  C  ->  A. x  A  =  C )
2 mpteq12f 4482 . 2  |-  ( ( A. x  A  =  C  /\  A. x  e.  A  B  =  D )  ->  (
x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
31, 2sylan 474 1  |-  ( ( A  =  C  /\  A. x  e.  A  B  =  D )  ->  (
x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371   A.wal 1444    = wceq 1446   A.wral 2739    |-> cmpt 4464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2744  df-opab 4465  df-mpt 4466
This theorem is referenced by:  mpteq1  4486  mpteqb  5969  fmptcof  6062  mapxpen  7743  prodeq2w  13978  prdsdsval2  15394  prdsdsval3  15395  ablfac2  17734  mdetunilem9  19657  mdetmul  19660  xkocnv  20841  voliun  22519  itgeq1f  22741  itgeq2  22747  iblcnlem  22758  esumeq2  28869  esumcvg  28919  dvtan  32004  bddiblnc  32024
  Copyright terms: Public domain W3C validator