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

Theorem mpt2eq3dva 5912
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 2294 . . . 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 5902 . 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 5863 . 2  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
7 df-mpt2 5863 . 2  |-  ( x  e.  A ,  y  e.  B  |->  D )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  D
) }
85, 6, 73eqtr4g 2340 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 1623    e. wcel 1684   {coprab 5859    e. cmpt2 5860
This theorem is referenced by:  mpt2eq3ia  5913  ofeq  6080  fmpt2co  6202  seqomeq12  6466  mapxpen  7027  cantnffval  7364  cantnfval  7369  cantnfres  7379  sadfval  12643  smufval  12668  vdwapfval  13018  comfeq  13609  monpropd  13640  cofuval2  13761  cofuass  13763  cofulid  13764  cofurid  13765  catcisolem  13938  prfval  13973  prf1st  13978  prf2nd  13979  1st2ndprf  13980  xpcpropd  13982  curf1  13999  curfuncf  14012  curf2ndf  14021  odumeet  14244  odujoin  14246  grpsubpropd2  14567  mulgpropd  14600  lsmfval  14949  oppglsm  14953  subglsm  14982  lsmpropd  14986  gsumcom2  15226  gsumdixp  15392  psrvscafval  16135  evlslem4  16245  evlslem2  16249  psrplusgpropd  16313  ptval2  17296  cnmpt2t  17367  cnmpt22  17368  cnmptcom  17372  cnmptk2  17380  cnmpt2plusg  17771  istgp2  17774  prdstmdd  17806  cnmpt2vsca  17877  cnmpt2ds  18348  cnmpt2pc  18426  cnmpt2ip  18675  nvmfval  21202  cvmlift2lem6  23250  cvmlift2lem7  23251  cvmlift2lem12  23256  iscst1  24586  dvhfvadd  30654
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-oprab 5862  df-mpt2 5863
  Copyright terms: Public domain W3C validator