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

Theorem mpteq12dv 4515
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 465 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
41, 3mpteq12dva 4514 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804    |-> cmpt 4495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-opab 4496  df-mpt 4497
This theorem is referenced by:  mpteq12i  4521  ovmpt3rab1  6519  offval  6532  offval3  6779  cantnffval  8083  cnfcomlem  8146  cnfcomlemOLD  8154  fseqenlem1  8408  dfac12lem1  8526  dfac12r  8529  ackbij2lem2  8623  ackbij2lem3  8624  r1om  8627  ccatfval  12573  swrdval  12625  revval  12715  odzval  14299  vdwpc  14479  restval  14805  prdsval  14833  imasval  14889  qusval  14920  mrcfval  14986  cidfval  15054  monfval  15108  ismon  15109  isepi  15116  idfuval  15223  resfval  15239  resfval2  15240  fucval  15305  homafval  15334  idafval  15362  prfval  15446  prf2fval  15448  curfval  15470  curfpropd  15480  hofval  15499  hof2fval  15502  yonedalem3a  15521  yonedalem4a  15522  yonedalem4c  15524  yonedainv  15528  lubfval  15586  glbfval  15599  ipoval  15762  grpinvfval  16066  grpinvpropd  16091  cntzfval  16336  pmtrfval  16453  psgnfval  16503  odfval  16535  sylow1lem2  16597  sylow1lem4  16599  sylow2blem1  16618  sylow3lem1  16625  sylow3lem2  16626  sylow3lem3  16627  sylow3lem6  16630  pj1fval  16690  vrgpfval  16762  gsum2dlem2  16976  gsum2dOLD  16978  gsum2d2  16980  dprdval  17012  dprdvalOLD  17014  dprd2dlem2  17067  dprd2dlem1  17068  dprd2da  17069  dprd2d2  17071  dpjfval  17082  srgbinom  17174  staffval  17474  lspfval  17597  lsppropd  17642  sraval  17800  aspval  17955  asclfval  17961  ressascl  17971  psrval  17989  psrass1lem  18007  psrmulval  18017  mvrfval  18054  opsrval  18117  mpfrcl  18165  evlsval  18166  coe1mul2  18288  cply1mul  18313  evls1fval  18334  evl1fval  18342  isphl  18640  ocvfval  18674  pjfval  18714  uvcfval  18792  mamufval  18864  mvmulfval  19021  marepvfval  19044  submafval  19058  mdetfval  19065  madufval  19116  minmar1fval  19125  mat2pmatfval  19201  cpm2mfval  19227  decpmatmullem  19249  decpmatmulsumfsupp  19251  pm2mpval  19273  pm2mpmhmlem1  19296  pm2mpmhmlem2  19297  chpmatfval  19308  ntrfval  19502  clsfval  19503  neifval  19577  lpfval  19616  ordtval  19667  ordtbas2  19669  ordtcnv  19679  ordtrest  19680  ordtrest2  19682  cnpfval  19712  kqval  20204  fmval  20421  fmf  20423  flffval  20467  fcfval  20511  cnextval  20538  tsmsval2  20605  nmfval  21086  nmpropd  21091  nmpropd2  21092  subgnm  21124  tngnm  21142  nmofval  21198  pi1xfrcnv  21534  iscph  21594  tchval  21638  limcfval  22253  dvfval  22278  eldv  22279  mdegfval  22437  mdegmullem  22455  mdegpropd  22461  coe1mul3  22477  ig1pval  22550  taylfval  22730  mirval  24012  ishpg  24104  lmif  24127  islmib  24129  vdgrfval  24871  grpoinvfval  25202  nmoofval  25653  eigvalfval  26792  ressnm  27616  ordtprsval  27877  ordtprsuni  27878  ordtrestNEW  27880  indv  28003  ofcfval  28074  ofcfval3  28078  omsval  28241  sitgval  28251  issibf  28252  sitgfval  28260  signstfv  28497  cvmliftlem5  28711  cvmliftlem15  28720  mvrsval  28842  mrsubffval  28844  elmrsubrn  28857  msubffval  28860  mvhfval  28870  msrfval  28874  tailfval  30165  hbtlem1  31047  hbtlem7  31049  rgspnval  31093  cytpval  31145  ply1mulgsumlem3  32723  ply1mulgsumlem4  32724  ply1mulgsum  32725  lincval  32745  lsatset  34455  lkrfval  34552  pmapfval  35220  pclfvalN  35353  polfvalN  35368  watfvalN  35456  ldilfset  35572  ltrnfset  35581  dilfsetN  35617  trnfsetN  35620  trlfset  35625  trlset  35626  tgrpfset  36210  tendofset  36224  erngfset  36265  erngset  36266  erngfset-rN  36273  erngset-rN  36274  dvafset  36470  diaffval  36497  diafval  36498  dvhfset  36547  docaffvalN  36588  docafvalN  36589  djaffvalN  36600  dibffval  36607  dibfval  36608  dicffval  36641  dicfval  36642  dihffval  36697  dochffval  36816  dochfval  36817  djhffval  36863  lcdfval  37055  mapdffval  37093  mapdfval  37094  hvmapffval  37225  hvmapfval  37226  hdmap1ffval  37263  hdmap1fval  37264  hdmapffval  37296  hdmapfval  37297  hgmapffval  37355  hgmapfval  37356  hlhilset  37404
  Copyright terms: Public domain W3C validator