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

Theorem mpt2eq3dva 6079
Description: Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
Hypothesis
Ref Expression
mpt2eq3dva.1  |-  ( (
ph  /\  x  e.  A  /\  y  e.  B
)  ->  C  =  D )
Assertion
Ref Expression
mpt2eq3dva  |-  ( ph  ->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A , 
y  e.  B  |->  D ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    A( x, y)    B( x, y)    C( x, y)    D( x, y)

Proof of Theorem mpt2eq3dva
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 mpt2eq3dva.1 . . . . . 6  |-  ( (
ph  /\  x  e.  A  /\  y  e.  B
)  ->  C  =  D )
213expb 1154 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  C  =  D )
32eqeq2d 2400 . . . 4  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( z  =  C  <-> 
z  =  D ) )
43pm5.32da 623 . . 3  |-  ( ph  ->  ( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) ) )
54oprabbidv 6069 . 2  |-  ( ph  ->  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  D ) } )
6 df-mpt2 6027 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
7 df-mpt2 6027 . 2  |-  ( x  e.  A ,  y  e.  B  |->  D )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) }
85, 6, 73eqtr4g 2446 1  |-  ( ph  ->  ( 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 359    /\ w3a 936    = wceq 1649    e. wcel 1717   {coprab 6023    e. cmpt2 6024
This theorem is referenced by:  mpt2eq3ia  6080  ofeq  6248  fmpt2co  6371  seqomeq12  6649  mapxpen  7211  cantnffval  7553  cantnfval  7558  cantnfres  7568  sadfval  12893  smufval  12918  vdwapfval  13268  comfeq  13861  monpropd  13892  cofuval2  14013  cofuass  14015  cofulid  14016  cofurid  14017  catcisolem  14190  prfval  14225  prf1st  14230  prf2nd  14231  1st2ndprf  14232  xpcpropd  14234  curf1  14251  curfuncf  14264  curf2ndf  14273  odumeet  14496  odujoin  14498  grpsubpropd2  14819  mulgpropd  14852  lsmfval  15201  oppglsm  15205  subglsm  15234  lsmpropd  15238  gsumcom2  15478  gsumdixp  15644  psrvscafval  16383  evlslem4  16493  evlslem2  16497  psrplusgpropd  16558  ptval2  17556  cnmpt2t  17628  cnmpt22  17629  cnmptcom  17633  cnmptk2  17641  cnmpt2plusg  18041  istgp2  18044  prdstmdd  18076  cnmpt2vsca  18147  cnmpt2ds  18747  cnmpt2pc  18826  cnmpt2ip  19075  nvmfval  21975  ofceq  24278  cvmlift2lem6  24776  cvmlift2lem7  24777  cvmlift2lem12  24782  dvhfvadd  31208
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-oprab 6026  df-mpt2 6027
  Copyright terms: Public domain W3C validator