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

Theorem mpt2eq12 5924
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 2296 . . . . 5  |-  E  =  E
21rgenw 2623 . . . 4  |-  A. y  e.  B  E  =  E
32jctr 526 . . 3  |-  ( B  =  D  ->  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
43ralrimivw 2640 . 2  |-  ( B  =  D  ->  A. x  e.  A  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
5 mpt2eq123 5923 . 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 460 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 358    = wceq 1632   A.wral 2556    e. cmpt2 5876
This theorem is referenced by:  dffi3  7200  cantnfres  7395  xpsval  13490  homffval  13610  comfffval  13617  monpropd  13656  natfval  13836  plusffval  14395  grpsubfval  14540  grpsubpropd2  14583  lsmvalx  14966  oppglsm  14969  lsmpropd  15002  dvrfval  15482  scaffval  15661  psrmulr  16145  psrplusgpropd  16329  ipffval  16568  txval  17275  cnmptk1p  17395  cnmptk2  17396  xpstopnlem1  17516  pcofval  18524  iscst2  25278  hmeogrp  25640  mendplusgfval  27596  mendmulrfval  27598  mendvscafval  27601
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-oprab 5878  df-mpt2 5879
  Copyright terms: Public domain W3C validator