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

Theorem mpt2eq3dva 6141
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 1155 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  C  =  D )
32eqeq2d 2449 . . . 4  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( z  =  C  <-> 
z  =  D ) )
43pm5.32da 624 . . 3  |-  ( ph  ->  ( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) ) )
54oprabbidv 6131 . 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 6089 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
7 df-mpt2 6089 . 2  |-  ( x  e.  A ,  y  e.  B  |->  D )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) }
85, 6, 73eqtr4g 2495 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 360    /\ w3a 937    = wceq 1653    e. wcel 1726   {coprab 6085    e. cmpt2 6086
This theorem is referenced by:  mpt2eq3ia  6142  ofeq  6310  fmpt2co  6433  seqomeq12  6714  mapxpen  7276  cantnffval  7621  cantnfval  7626  cantnfres  7636  sadfval  12969  smufval  12994  vdwapfval  13344  comfeq  13937  monpropd  13968  cofuval2  14089  cofuass  14091  cofulid  14092  cofurid  14093  catcisolem  14266  prfval  14301  prf1st  14306  prf2nd  14307  1st2ndprf  14308  xpcpropd  14310  curf1  14327  curfuncf  14340  curf2ndf  14349  odumeet  14572  odujoin  14574  grpsubpropd2  14895  mulgpropd  14928  lsmfval  15277  oppglsm  15281  subglsm  15310  lsmpropd  15314  gsumcom2  15554  gsumdixp  15720  psrvscafval  16459  evlslem4  16569  evlslem2  16573  psrplusgpropd  16634  ptval2  17638  cnmpt2t  17710  cnmpt22  17711  cnmptcom  17715  cnmptk2  17723  cnmpt2plusg  18123  istgp2  18126  prdstmdd  18158  cnmpt2vsca  18229  cnmpt2ds  18879  cnmpt2pc  18958  cnmpt2ip  19207  nvmfval  22130  pstmval  24295  ofceq  24485  cvmlift2lem6  25000  cvmlift2lem7  25001  cvmlift2lem12  25006  dvhfvadd  31963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-oprab 6088  df-mpt2 6089
  Copyright terms: Public domain W3C validator