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

Theorem mpt2eq3ia 6151
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 1006 . . 3  |-  ( ( T.  /\  x  e.  A  /\  y  e.  B )  ->  C  =  D )
32mpt2eq3dva 6150 . 2  |-  ( T. 
->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A , 
y  e.  B  |->  D ) )
43trud 1378 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 1369   T. wtru 1370    e. wcel 1756    e. cmpt2 6093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-oprab 6095  df-mpt2 6096
This theorem is referenced by:  mpt2difsnif  6183  mpt2snif  6184  oprab2co  6658  cnfcomlem  7932  cnfcom2  7935  cnfcomlemOLD  7940  cnfcom2OLD  7943  dfioo2  11390  sadcom  13659  comfffval2  14640  oppchomf  14659  symgga  15911  oppglsm  16141  dfrhm2  16808  cnfldsub  17844  cnflddiv  17846  mat0op  18320  mattpos1  18340  mdetrsca2  18411  mdetrlin2  18413  mdetunilem5  18422  mdetunilem7  18424  madufval  18443  maducoeval2  18446  madugsum  18449  leordtval  18817  xpstopnlem1  19382  divcn  20444  oprpiece1res1  20523  oprpiece1res2  20524  cxpcn  22183  cnnvm  24073  cnre2csqima  26341  mndpluscn  26356  raddcn  26359  mendplusgfval  29542  elovmpt2wrd  30256  wwlknprop  30320  numclwwlk5  30705  numclwwlk7  30707  pmatcollpw1dst  30901  pmatcollpw2lem  30905  pmattomply1lem  30908  mp2pm2mplem3  30918  mp2pm2mplem5  30920  mp2pm2mp  30921  dflinc2  30944
  Copyright terms: Public domain W3C validator