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

Theorem mpteq12dv 4358
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 462 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
41, 3mpteq12dva 4357 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755    e. cmpt 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-opab 4339  df-mpt 4340
This theorem is referenced by:  mpteq12i  4364  offval  6316  offval3  6560  cantnffval  7857  cnfcomlem  7920  cnfcomlemOLD  7928  fseqenlem1  8182  dfac12lem1  8300  dfac12r  8303  ackbij2lem2  8397  ackbij2lem3  8398  r1om  8401  ccatfval  12257  swrdval  12297  revval  12384  odzval  13846  vdwpc  14024  restval  14348  prdsval  14376  imasval  14432  divsval  14463  mrcfval  14529  cidfval  14597  monfval  14654  ismon  14655  isepi  14662  idfuval  14769  resfval  14785  resfval2  14786  fucval  14851  homafval  14880  idafval  14908  prfval  14992  prf2fval  14994  curfval  15016  curfpropd  15026  hofval  15045  hof2fval  15048  yonedalem3a  15067  yonedalem4a  15068  yonedalem4c  15070  yonedainv  15074  lubfval  15131  glbfval  15144  ipoval  15307  grpinvfval  15556  grpinvpropd  15581  cntzfval  15818  pmtrfval  15936  psgnfval  15986  odfval  16016  sylow1lem2  16078  sylow1lem4  16080  sylow2blem1  16099  sylow3lem1  16106  sylow3lem2  16107  sylow3lem3  16108  sylow3lem6  16111  pj1fval  16171  vrgpfval  16243  gsum2dlem2  16436  gsum2dOLD  16438  gsum2d2  16440  dprdval  16459  dprdvalOLD  16461  dprd2dlem2  16513  dprd2dlem1  16514  dprd2da  16515  dprd2d2  16517  dpjfval  16528  staffval  16856  lspfval  16976  lsppropd  17021  sraval  17179  aspval  17321  asclfval  17327  ressascl  17336  psrval  17363  psrass1lem  17381  psrmulval  17391  mvrfval  17427  opsrval  17488  coe1mul2  17621  isphl  17899  ocvfval  17933  pjfval  17973  uvcfval  18051  mamufval  18125  mvmulfval  18195  marepvfval  18218  submafval  18232  mdetfval  18239  madufval  18285  minmar1fval  18294  ntrfval  18470  clsfval  18471  neifval  18545  lpfval  18584  ordtval  18635  ordtbas2  18637  ordtcnv  18647  ordtrest  18648  ordtrest2  18650  cnpfval  18680  kqval  19141  fmval  19358  fmf  19360  flffval  19404  fcfval  19448  cnextval  19475  tsmsval2  19542  nmfval  20023  nmpropd  20028  nmpropd2  20029  subgnm  20061  tngnm  20079  nmofval  20135  pi1xfrcnv  20471  iscph  20531  tchval  20575  limcfval  21189  dvfval  21214  eldv  21215  mpfrcl  21370  evlsval  21371  evl1fval  21378  mdegfval  21416  mdegmullem  21434  mdegpropd  21440  coe1mul3  21456  ig1pval  21529  taylfval  21709  mirval  22925  vdgrfval  23388  grpoinvfval  23534  nmoofval  23985  eigvalfval  25124  ressnm  25935  ordtprsval  26202  ordtprsuni  26203  ordtcnvNEW  26204  ordtrestNEW  26205  ordtrest2NEW  26207  xrhval  26298  indv  26323  ofcfval  26394  ofcfval3  26398  sitgval  26566  issibf  26567  sitgfval  26575  signstfv  26812  cvmliftlem5  27026  cvmliftlem15  27035  tailfval  28437  hbtlem1  29324  hbtlem7  29326  rgspnval  29370  cytpval  29422  ovmpt3rab1  30007  lincval  30673  lsatset  32229  lkrfval  32326  pmapfval  32994  pclfvalN  33127  polfvalN  33142  watfvalN  33230  ldilfset  33346  ltrnfset  33355  dilfsetN  33390  trnfsetN  33393  trlfset  33398  trlset  33399  tgrpfset  33982  tendofset  33996  erngfset  34037  erngset  34038  erngfset-rN  34045  erngset-rN  34046  dvafset  34242  diaffval  34269  diafval  34270  dvhfset  34319  docaffvalN  34360  docafvalN  34361  djaffvalN  34372  dibffval  34379  dibfval  34380  dicffval  34413  dicfval  34414  dihffval  34469  dochffval  34588  dochfval  34589  djhffval  34635  lcdfval  34827  mapdffval  34865  mapdfval  34866  hvmapffval  34997  hvmapfval  34998  hdmap1ffval  35035  hdmap1fval  35036  hdmapffval  35068  hdmapfval  35069  hgmapffval  35127  hgmapfval  35128  hlhilset  35176
  Copyright terms: Public domain W3C validator