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

Theorem mpteq12dv 4229
Description: An equality inference for the maps to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq12dv.1  |-  ( ph  ->  A  =  C )
mpteq12dv.2  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
mpteq12dv  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    B( x)    C( x)    D( x)

Proof of Theorem mpteq12dv
StepHypRef Expression
1 mpteq12dv.1 . 2  |-  ( ph  ->  A  =  C )
2 mpteq12dv.2 . . 3  |-  ( ph  ->  B  =  D )
32adantr 452 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
41, 3mpteq12dva 4228 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717    e. cmpt 4208
This theorem is referenced by:  mpteq12i  4235  offval  6252  offval3  6258  cantnffval  7552  cnfcomlem  7590  fseqenlem1  7839  dfac12lem1  7957  dfac12r  7960  ackbij2lem2  8054  ackbij2lem3  8055  r1om  8058  ccatfval  11670  swrdval  11692  revval  11720  odzval  13105  vdwpc  13276  restval  13582  prdsval  13606  imasval  13665  divsval  13695  mrcfval  13761  cidfval  13829  monfval  13886  ismon  13887  isepi  13894  idfuval  14001  resfval  14017  resfval2  14018  fucval  14083  homafval  14112  idafval  14140  prfval  14224  prf2fval  14226  curfval  14248  curfpropd  14258  hofval  14277  hof2fval  14280  yonedalem3a  14299  yonedalem4a  14300  yonedalem4c  14302  yonedainv  14306  lubfval  14363  glbfval  14368  ipoval  14508  grpinvfval  14771  grpinvpropd  14794  cntzfval  15047  odfval  15099  sylow1lem2  15161  sylow1lem4  15163  sylow2blem1  15182  sylow3lem1  15189  sylow3lem2  15190  sylow3lem3  15191  sylow3lem6  15194  pj1fval  15254  vrgpfval  15326  gsum2d  15474  gsum2d2  15476  dprdval  15489  dprd2dlem2  15526  dprd2dlem1  15527  dprd2da  15528  dprd2d2  15530  dpjfval  15541  staffval  15863  lspfval  15977  lsppropd  16022  sraval  16176  aspval  16315  asclfval  16321  ressascl  16330  psrval  16357  psrass1lem  16370  psrmulval  16378  mvrfval  16412  opsrval  16463  coe1mul2  16590  isphl  16783  ocvfval  16817  pjfval  16857  ntrfval  17012  clsfval  17013  neifval  17087  lpfval  17126  ordtval  17176  ordtbas2  17178  ordtcnv  17188  ordtrest  17189  ordtrest2  17191  cnpfval  17221  kqval  17680  fmval  17897  fmf  17899  flffval  17943  fcfval  17987  cnextval  18014  tsmsval2  18081  nmfval  18508  nmpropd  18513  nmpropd2  18514  subgnm  18546  tngnm  18564  nmofval  18620  pi1xfrcnv  18954  iscph  19005  tchval  19049  limcfval  19627  dvfval  19652  eldv  19653  mpfrcl  19807  evlsval  19808  evl1fval  19815  mdegfval  19853  mdegmullem  19869  mdegpropd  19875  coe1mul3  19890  ig1pval  19963  taylfval  20143  vdgrfval  21515  grpoinvfval  21661  nmoofval  22112  eigvalfval  23249  ressnm  24024  indv  24207  ofcfval  24278  ofcfval3  24282  cvmliftlem5  24756  cvmliftlem15  24765  tailfval  26093  uvcfval  26903  hbtlem1  26997  hbtlem7  26999  rgspnval  27043  pmtrfval  27063  psgnfval  27093  mamufval  27113  mdetfval  27157  cytpval  27198  lsatset  29106  lkrfval  29203  pmapfval  29871  pclfvalN  30004  polfvalN  30019  watfvalN  30107  ldilfset  30223  ltrnfset  30232  dilfsetN  30267  trnfsetN  30270  trlfset  30275  trlset  30276  tgrpfset  30859  tendofset  30873  erngfset  30914  erngset  30915  erngfset-rN  30922  erngset-rN  30923  dvafset  31119  diaffval  31146  diafval  31147  dvhfset  31196  docaffvalN  31237  docafvalN  31238  djaffvalN  31249  dibffval  31256  dibfval  31257  dicffval  31290  dicfval  31291  dihffval  31346  dochffval  31465  dochfval  31466  djhffval  31512  lcdfval  31704  mapdffval  31742  mapdfval  31743  hvmapffval  31874  hvmapfval  31875  hdmap1ffval  31912  hdmap1fval  31913  hdmapffval  31945  hdmapfval  31946  hgmapffval  32004  hgmapfval  32005  hlhilset  32053
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 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-ral 2655  df-opab 4209  df-mpt 4210
  Copyright terms: Public domain W3C validator