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

Theorem mpt2eq3ia 5913
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 5912 . 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 1623    e. wcel 1684    e. cmpt2 5860
This theorem is referenced by:  oprab2co  6204  cnfcomlem  7402  cnfcom2  7405  dfioo2  10744  sadcom  12654  comfffval2  13604  oppchomf  13623  symgga  14786  oppglsm  14953  dfrhm2  15498  cnfldsub  16402  cnflddiv  16404  leordtval  16943  xpstopnlem1  17500  divcn  18372  oprpiece1res1  18449  oprpiece1res2  18450  cxpcn  20085  cnnvm  21251  cnre2csqima  23295  mndpluscn  23299  raddcn  23302  mendplusgfval  27493
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-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-oprab 5862  df-mpt2 5863
  Copyright terms: Public domain W3C validator