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

Theorem mpt2eq3ia 6370
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 1023 . . 3  |-  ( ( T.  /\  x  e.  A  /\  y  e.  B )  ->  C  =  D )
32mpt2eq3dva 6369 . 2  |-  ( T. 
->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A , 
y  e.  B  |->  D ) )
43trud 1446 1  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   T. wtru 1438    e. wcel 1870    |-> cmpt2 6307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-oprab 6309  df-mpt2 6310
This theorem is referenced by:  mpt2difsnif  6403  mpt2snif  6404  oprab2co  6892  cnfcomlem  8203  cnfcom2  8206  dfioo2  11735  elovmpt2wrd  12696  sadcom  14411  comfffval2  15557  oppchomf  15576  symgga  16998  oppglsm  17229  dfrhm2  17880  cnfldsub  18931  cnflddiv  18933  mat0op  19375  mattpos1  19412  mdetunilem7  19574  madufval  19593  maducoeval2  19596  madugsum  19599  mp2pm2mplem5  19765  mp2pm2mp  19766  leordtval  20160  xpstopnlem1  20755  divcn  21796  oprpiece1res1  21875  oprpiece1res2  21876  cxpcn  23550  wwlknprop  25259  numclwwlk5  25685  numclwwlk7  25687  cnnvm  26159  mdetpmtr2  28489  madjusmdetlem1  28492  cnre2csqima  28556  mndpluscn  28571  raddcn  28574  icorempt2  31488  mendplusgfval  35749  dflinc2  38962
  Copyright terms: Public domain W3C validator