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

Theorem mpteq12dv 4247
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 4246 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721    e. cmpt 4226
This theorem is referenced by:  mpteq12i  4253  offval  6271  offval3  6277  cantnffval  7574  cnfcomlem  7612  fseqenlem1  7861  dfac12lem1  7979  dfac12r  7982  ackbij2lem2  8076  ackbij2lem3  8077  r1om  8080  ccatfval  11697  swrdval  11719  revval  11747  odzval  13132  vdwpc  13303  restval  13609  prdsval  13633  imasval  13692  divsval  13722  mrcfval  13788  cidfval  13856  monfval  13913  ismon  13914  isepi  13921  idfuval  14028  resfval  14044  resfval2  14045  fucval  14110  homafval  14139  idafval  14167  prfval  14251  prf2fval  14253  curfval  14275  curfpropd  14285  hofval  14304  hof2fval  14307  yonedalem3a  14326  yonedalem4a  14327  yonedalem4c  14329  yonedainv  14333  lubfval  14390  glbfval  14395  ipoval  14535  grpinvfval  14798  grpinvpropd  14821  cntzfval  15074  odfval  15126  sylow1lem2  15188  sylow1lem4  15190  sylow2blem1  15209  sylow3lem1  15216  sylow3lem2  15217  sylow3lem3  15218  sylow3lem6  15221  pj1fval  15281  vrgpfval  15353  gsum2d  15501  gsum2d2  15503  dprdval  15516  dprd2dlem2  15553  dprd2dlem1  15554  dprd2da  15555  dprd2d2  15557  dpjfval  15568  staffval  15890  lspfval  16004  lsppropd  16049  sraval  16203  aspval  16342  asclfval  16348  ressascl  16357  psrval  16384  psrass1lem  16397  psrmulval  16405  mvrfval  16439  opsrval  16490  coe1mul2  16617  isphl  16814  ocvfval  16848  pjfval  16888  ntrfval  17043  clsfval  17044  neifval  17118  lpfval  17157  ordtval  17207  ordtbas2  17209  ordtcnv  17219  ordtrest  17220  ordtrest2  17222  cnpfval  17252  kqval  17711  fmval  17928  fmf  17930  flffval  17974  fcfval  18018  cnextval  18045  tsmsval2  18112  nmfval  18589  nmpropd  18594  nmpropd2  18595  subgnm  18627  tngnm  18645  nmofval  18701  pi1xfrcnv  19035  iscph  19086  tchval  19130  limcfval  19712  dvfval  19737  eldv  19738  mpfrcl  19892  evlsval  19893  evl1fval  19900  mdegfval  19938  mdegmullem  19954  mdegpropd  19960  coe1mul3  19975  ig1pval  20048  taylfval  20228  vdgrfval  21619  grpoinvfval  21765  nmoofval  22216  eigvalfval  23353  ressnm  24137  xrhval  24337  indv  24363  ofcfval  24434  ofcfval3  24438  sitgval  24600  issibf  24601  sitgfval  24608  cvmliftlem5  24929  cvmliftlem15  24938  tailfval  26291  uvcfval  27101  hbtlem1  27195  hbtlem7  27197  rgspnval  27241  pmtrfval  27261  psgnfval  27291  mamufval  27311  mdetfval  27355  cytpval  27396  lsatset  29473  lkrfval  29570  pmapfval  30238  pclfvalN  30371  polfvalN  30386  watfvalN  30474  ldilfset  30590  ltrnfset  30599  dilfsetN  30634  trnfsetN  30637  trlfset  30642  trlset  30643  tgrpfset  31226  tendofset  31240  erngfset  31281  erngset  31282  erngfset-rN  31289  erngset-rN  31290  dvafset  31486  diaffval  31513  diafval  31514  dvhfset  31563  docaffvalN  31604  docafvalN  31605  djaffvalN  31616  dibffval  31623  dibfval  31624  dicffval  31657  dicfval  31658  dihffval  31713  dochffval  31832  dochfval  31833  djhffval  31879  lcdfval  32071  mapdffval  32109  mapdfval  32110  hvmapffval  32241  hvmapfval  32242  hdmap1ffval  32279  hdmap1fval  32280  hdmapffval  32312  hdmapfval  32313  hgmapffval  32371  hgmapfval  32372  hlhilset  32420
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-ral 2671  df-opab 4227  df-mpt 4228
  Copyright terms: Public domain W3C validator