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

Theorem mpt2eq12 6352
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 2467 . . . . 5  |-  E  =  E
21rgenw 2828 . . . 4  |-  A. y  e.  B  E  =  E
32jctr 542 . . 3  |-  ( B  =  D  ->  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
43ralrimivw 2882 . 2  |-  ( B  =  D  ->  A. x  e.  A  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
5 mpt2eq123 6351 . 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 1379   A.wral 2817    |-> cmpt2 6297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-oprab 6299  df-mpt2 6300
This theorem is referenced by:  dffi3  7903  cantnfres  8108  xpsval  14844  homffval  14964  comfffval  14971  monpropd  15010  natfval  15190  plusffval  15751  grpsubfval  15964  grpsubpropd2  16013  lsmvalx  16532  oppglsm  16535  lsmpropd  16568  dvrfval  17205  scaffval  17401  psrmulr  17907  psrplusgpropd  18147  ipffval  18552  marrepfval  18931  marepvfval  18936  d1mat2pmat  19109  txval  19933  cnmptk1p  20054  cnmptk2  20055  xpstopnlem1  20178  pcofval  21378  rrxmval  21700  pstmval  27690  qqhval2  27779  mendplusgfval  31054  mendmulrfval  31056  mendvscafval  31059  lmod1zr  32531
  Copyright terms: Public domain W3C validator