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

Theorem mpt2eq12 5908
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 2283 . . . . 5  |-  E  =  E
21rgenw 2610 . . . 4  |-  A. y  e.  B  E  =  E
32jctr 526 . . 3  |-  ( B  =  D  ->  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
43ralrimivw 2627 . 2  |-  ( B  =  D  ->  A. x  e.  A  ( B  =  D  /\  A. y  e.  B  E  =  E ) )
5 mpt2eq123 5907 . 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 1623   A.wral 2543    e. cmpt2 5860
This theorem is referenced by:  dffi3  7184  cantnfres  7379  xpsval  13474  homffval  13594  comfffval  13601  monpropd  13640  natfval  13820  plusffval  14379  grpsubfval  14524  grpsubpropd2  14567  lsmvalx  14950  oppglsm  14953  lsmpropd  14986  dvrfval  15466  scaffval  15645  psrmulr  16129  psrplusgpropd  16313  ipffval  16552  txval  17259  cnmptk1p  17379  cnmptk2  17380  xpstopnlem1  17500  pcofval  18508  iscst2  25175  hmeogrp  25537  mendplusgfval  27493  mendmulrfval  27495  mendvscafval  27498
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-oprab 5862  df-mpt2 5863
  Copyright terms: Public domain W3C validator