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

Theorem mpt2eq3ia 6337
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 1009 . . 3  |-  ( ( T.  /\  x  e.  A  /\  y  e.  B )  ->  C  =  D )
32mpt2eq3dva 6336 . 2  |-  ( T. 
->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A , 
y  e.  B  |->  D ) )
43trud 1383 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 369    = wceq 1374   T. wtru 1375    e. wcel 1762    |-> cmpt2 6277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-oprab 6279  df-mpt2 6280
This theorem is referenced by:  mpt2difsnif  6370  mpt2snif  6371  oprab2co  6858  cnfcomlem  8132  cnfcom2  8135  cnfcomlemOLD  8140  cnfcom2OLD  8143  dfioo2  11614  elovmpt2wrd  12535  sadcom  13961  comfffval2  14946  oppchomf  14965  symgga  16219  oppglsm  16451  dfrhm2  17143  cnfldsub  18210  cnflddiv  18212  mat0op  18681  mattpos1  18718  mdetrsca2  18866  mdetrlin2  18869  mdetunilem5  18878  mdetunilem7  18880  madufval  18899  maducoeval2  18902  madugsum  18905  mp2pm2mplem5  19071  mp2pm2mp  19072  leordtval  19473  xpstopnlem1  20038  divcn  21100  oprpiece1res1  21179  oprpiece1res2  21180  cxpcn  22840  wwlknprop  24348  numclwwlk5  24775  numclwwlk7  24777  cnnvm  25250  cnre2csqima  27515  mndpluscn  27530  raddcn  27533  mendplusgfval  30728  dflinc2  31959
  Copyright terms: Public domain W3C validator