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

Theorem mpt2eq3dva 5928
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 1152 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  C  =  D )
32eqeq2d 2307 . . . 4  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( z  =  C  <-> 
z  =  D ) )
43pm5.32da 622 . . 3  |-  ( ph  ->  ( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) ) )
54oprabbidv 5918 . 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 5879 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
7 df-mpt2 5879 . 2  |-  ( x  e.  A ,  y  e.  B  |->  D )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) }
85, 6, 73eqtr4g 2353 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 358    /\ w3a 934    = wceq 1632    e. wcel 1696   {coprab 5875    e. cmpt2 5876
This theorem is referenced by:  mpt2eq3ia  5929  ofeq  6096  fmpt2co  6218  seqomeq12  6482  mapxpen  7043  cantnffval  7380  cantnfval  7385  cantnfres  7395  sadfval  12659  smufval  12684  vdwapfval  13034  comfeq  13625  monpropd  13656  cofuval2  13777  cofuass  13779  cofulid  13780  cofurid  13781  catcisolem  13954  prfval  13989  prf1st  13994  prf2nd  13995  1st2ndprf  13996  xpcpropd  13998  curf1  14015  curfuncf  14028  curf2ndf  14037  odumeet  14260  odujoin  14262  grpsubpropd2  14583  mulgpropd  14616  lsmfval  14965  oppglsm  14969  subglsm  14998  lsmpropd  15002  gsumcom2  15242  gsumdixp  15408  psrvscafval  16151  evlslem4  16261  evlslem2  16265  psrplusgpropd  16329  ptval2  17312  cnmpt2t  17383  cnmpt22  17384  cnmptcom  17388  cnmptk2  17396  cnmpt2plusg  17787  istgp2  17790  prdstmdd  17822  cnmpt2vsca  17893  cnmpt2ds  18364  cnmpt2pc  18442  cnmpt2ip  18691  nvmfval  21218  ofceq  23473  dya2iocrrnval  23597  cvmlift2lem6  23854  cvmlift2lem7  23855  cvmlift2lem12  23860  iscst1  25277  dvhfvadd  31903
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-oprab 5878  df-mpt2 5879
  Copyright terms: Public domain W3C validator