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

Theorem mpteq12 4501
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 1749 . 2  |-  ( A  =  C  ->  A. x  A  =  C )
2 mpteq12f 4498 . 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 1436    = wceq 1438   A.wral 2776    |-> cmpt 4480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-ral 2781  df-opab 4481  df-mpt 4482
This theorem is referenced by:  mpteq1  4502  mpteqb  5978  fmptcof  6070  mapxpen  7742  prodeq2w  13959  prdsdsval2  15375  prdsdsval3  15376  ablfac2  17715  mdetunilem9  19637  mdetmul  19640  xkocnv  20821  voliun  22499  itgeq1f  22721  itgeq2  22727  iblcnlem  22738  esumeq2  28859  esumcvg  28909  dvtan  31950  bddiblnc  31970
  Copyright terms: Public domain W3C validator