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

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

Proof of Theorem mpt2eq12
StepHypRef Expression
1 eqid 2435 . . . . 5  |-  E  =  E
21rgenw 2765 . . . 4  |-  A. y  e.  B  E  =  E
32jctr 527 . . 3  |-  ( B  =  D  ->  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
43ralrimivw 2782 . 2  |-  ( B  =  D  ->  A. x  e.  A  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
5 mpt2eq123 6125 . 2  |-  ( ( A  =  C  /\  A. x  e.  A  ( B  =  D  /\  A. y  e.  B  E  =  E ) )  -> 
( x  e.  A ,  y  e.  B  |->  E )  =  ( x  e.  C , 
y  e.  D  |->  E ) )
64, 5sylan2 461 1  |-  ( ( A  =  C  /\  B  =  D )  ->  ( x  e.  A ,  y  e.  B  |->  E )  =  ( x  e.  C , 
y  e.  D  |->  E ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652   A.wral 2697    e. cmpt2 6075
This theorem is referenced by:  dffi3  7428  cantnfres  7625  xpsval  13789  homffval  13909  comfffval  13916  monpropd  13955  natfval  14135  plusffval  14694  grpsubfval  14839  grpsubpropd2  14882  lsmvalx  15265  oppglsm  15268  lsmpropd  15301  dvrfval  15781  scaffval  15960  psrmulr  16440  psrplusgpropd  16621  ipffval  16871  txval  17588  cnmptk1p  17709  cnmptk2  17710  xpstopnlem1  17833  pcofval  19027  pstmval  24282  qqhval2  24358  mendplusgfval  27461  mendmulrfval  27463  mendvscafval  27466
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-oprab 6077  df-mpt2 6078
  Copyright terms: Public domain W3C validator