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

Theorem mpt2eq3dva 6130
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 2446 . . . 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 6120 . 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 6078 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
7 df-mpt2 6078 . 2  |-  ( x  e.  A ,  y  e.  B  |->  D )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) }
85, 6, 73eqtr4g 2492 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 1652    e. wcel 1725   {coprab 6074    e. cmpt2 6075
This theorem is referenced by:  mpt2eq3ia  6131  ofeq  6299  fmpt2co  6422  seqomeq12  6703  mapxpen  7265  cantnffval  7610  cantnfval  7615  cantnfres  7625  sadfval  12956  smufval  12981  vdwapfval  13331  comfeq  13924  monpropd  13955  cofuval2  14076  cofuass  14078  cofulid  14079  cofurid  14080  catcisolem  14253  prfval  14288  prf1st  14293  prf2nd  14294  1st2ndprf  14295  xpcpropd  14297  curf1  14314  curfuncf  14327  curf2ndf  14336  odumeet  14559  odujoin  14561  grpsubpropd2  14882  mulgpropd  14915  lsmfval  15264  oppglsm  15268  subglsm  15297  lsmpropd  15301  gsumcom2  15541  gsumdixp  15707  psrvscafval  16446  evlslem4  16556  evlslem2  16560  psrplusgpropd  16621  ptval2  17625  cnmpt2t  17697  cnmpt22  17698  cnmptcom  17702  cnmptk2  17710  cnmpt2plusg  18110  istgp2  18113  prdstmdd  18145  cnmpt2vsca  18216  cnmpt2ds  18866  cnmpt2pc  18945  cnmpt2ip  19194  nvmfval  22117  pstmval  24282  ofceq  24472  cvmlift2lem6  24987  cvmlift2lem7  24988  cvmlift2lem12  24993  dvhfvadd  31826
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-oprab 6077  df-mpt2 6078
  Copyright terms: Public domain W3C validator