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

Theorem mpt2eq12 6145
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 2442 . . . . 5  |-  E  =  E
21rgenw 2782 . . . 4  |-  A. y  e.  B  E  =  E
32jctr 542 . . 3  |-  ( B  =  D  ->  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
43ralrimivw 2799 . 2  |-  ( B  =  D  ->  A. x  e.  A  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
5 mpt2eq123 6144 . 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 474 1  |-  ( ( A  =  C  /\  B  =  D )  ->  ( x  e.  A ,  y  e.  B  |->  E )  =  ( x  e.  C , 
y  e.  D  |->  E ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369   A.wral 2714    e. cmpt2 6092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2719  df-oprab 6094  df-mpt2 6095
This theorem is referenced by:  dffi3  7680  cantnfres  7884  xpsval  14509  homffval  14629  comfffval  14636  monpropd  14675  natfval  14855  plusffval  15426  grpsubfval  15579  grpsubpropd2  15626  lsmvalx  16137  oppglsm  16140  lsmpropd  16173  dvrfval  16775  scaffval  16965  psrmulr  17454  psrplusgpropd  17689  ipffval  18076  marrepfval  18370  marepvfval  18375  txval  19136  cnmptk1p  19257  cnmptk2  19258  xpstopnlem1  19381  pcofval  20581  rrxmval  20903  pstmval  26321  qqhval2  26410  mendplusgfval  29540  mendmulrfval  29542  mendvscafval  29545  lmod1zr  31033
  Copyright terms: Public domain W3C validator