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

Theorem mpt2eq3ia 5929
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Hypothesis
Ref Expression
mpt2eq3ia.1  |-  ( ( x  e.  A  /\  y  e.  B )  ->  C  =  D )
Assertion
Ref Expression
mpt2eq3ia  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )

Proof of Theorem mpt2eq3ia
StepHypRef Expression
1 mpt2eq3ia.1 . . . 4  |-  ( ( x  e.  A  /\  y  e.  B )  ->  C  =  D )
213adant1 973 . . 3  |-  ( (  T.  /\  x  e.  A  /\  y  e.  B )  ->  C  =  D )
32mpt2eq3dva 5928 . 2  |-  (  T. 
->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A , 
y  e.  B  |->  D ) )
43trud 1314 1  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    T. wtru 1307    = wceq 1632    e. wcel 1696    e. cmpt2 5876
This theorem is referenced by:  oprab2co  6220  cnfcomlem  7418  cnfcom2  7421  dfioo2  10760  sadcom  12670  comfffval2  13620  oppchomf  13639  symgga  14802  oppglsm  14969  dfrhm2  15514  cnfldsub  16418  cnflddiv  16420  leordtval  16959  xpstopnlem1  17516  divcn  18388  oprpiece1res1  18465  oprpiece1res2  18466  cxpcn  20101  cnnvm  21267  cnre2csqima  23310  mndpluscn  23314  raddcn  23317  mendplusgfval  27596
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-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-oprab 5878  df-mpt2 5879
  Copyright terms: Public domain W3C validator