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

Theorem mpteq12 4482
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 1671 . 2  |-  ( A  =  C  ->  A. x  A  =  C )
2 mpteq12f 4479 . 2  |-  ( ( A. x  A  =  C  /\  A. x  e.  A  B  =  D )  ->  (
x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
31, 2sylan 471 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 369   A.wal 1368    = wceq 1370   A.wral 2799    |-> cmpt 4461
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-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2804  df-opab 4462  df-mpt 4463
This theorem is referenced by:  mpteq1  4483  mpteqb  5900  fmptcof  5989  mapxpen  7590  prdsdsval2  14544  prdsdsval3  14545  ablfac2  16715  mdetunilem9  18561  mdetmul  18564  xkocnv  19522  voliun  21171  itgeq1f  21385  itgeq2  21391  iblcnlem  21402  esumeq2  26657  esumcvg  26700  prodeq2w  27589  dvtan  28610  bddiblnc  28630
  Copyright terms: Public domain W3C validator