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

Theorem mpteq12dv 4698
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 (𝜑𝐴 = 𝐶)
mpteq12dv.2 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
mpteq12dv (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12dv
StepHypRef Expression
1 mpteq12dv.1 . 2 (𝜑𝐴 = 𝐶)
2 mpteq12dv.2 . . 3 (𝜑𝐵 = 𝐷)
32adantr 481 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
41, 3mpteq12dva 4697 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  cmpt 4678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-opab 4679  df-mpt 4680
This theorem is referenced by:  mpteq12i  4707  ovmpt3rab1  6851  offval  6864  offval3  7114  cantnffval  8512  cnfcomlem  8548  fseqenlem1  8799  dfac12lem1  8917  dfac12r  8920  ackbij2lem2  9014  ackbij2lem3  9015  r1om  9018  ccatfval  13305  swrdval  13363  revval  13454  odzval  15431  vdwpc  15619  restval  16019  prdsval  16047  imasval  16103  qusval  16134  mrcfval  16200  cidfval  16269  monfval  16324  ismon  16325  isepi  16332  idfuval  16468  resfval  16484  resfval2  16485  fucval  16550  homafval  16611  idafval  16639  prfval  16771  prf2fval  16773  curfval  16795  curfpropd  16805  hofval  16824  hof2fval  16827  yonedalem3a  16846  yonedalem4a  16847  yonedalem4c  16849  yonedainv  16853  lubfval  16910  glbfval  16923  ipoval  17086  grpinvfval  17392  grpinvpropd  17422  cntzfval  17685  pmtrfval  17802  psgnfval  17852  odfval  17884  sylow1lem2  17946  sylow1lem4  17948  sylow2blem1  17967  sylow3lem1  17974  sylow3lem2  17975  sylow3lem3  17976  sylow3lem6  17979  pj1fval  18039  vrgpfval  18111  gsum2dlem2  18302  gsum2d2  18305  dprdval  18334  dprd2dlem2  18371  dprd2dlem1  18372  dprd2da  18373  dprd2d2  18375  dpjfval  18386  srgbinom  18477  staffval  18779  lspfval  18905  lsppropd  18950  sraval  19108  aspval  19260  asclfval  19266  ressascl  19276  psrval  19294  psrass1lem  19309  psrmulval  19318  mvrfval  19352  opsrval  19406  mpfrcl  19450  evlsval  19451  coe1mul2  19571  cply1mul  19596  evls1fval  19616  evl1fval  19624  isphl  19905  ocvfval  19942  pjfval  19982  uvcfval  20055  mamufval  20123  mvmulfval  20280  marepvfval  20303  submafval  20317  mdetfval  20324  madufval  20375  minmar1fval  20384  mat2pmatfval  20460  cpm2mfval  20486  decpmatmullem  20508  decpmatmulsumfsupp  20510  pm2mpval  20532  pm2mpmhmlem1  20555  pm2mpmhmlem2  20556  chpmatfval  20567  ntrfval  20751  clsfval  20752  neifval  20826  lpfval  20865  ordtval  20916  ordtbas2  20918  ordtcnv  20928  ordtrest  20929  ordtrest2  20931  cnpfval  20961  kqval  21452  fmval  21670  fmf  21672  flffval  21716  fcfval  21760  cnextval  21788  tsmsval2  21856  nmfval  22316  nmpropd  22321  nmpropd2  22322  subgnm  22360  tngnm  22378  nmofval  22441  pi1xfrcnv  22780  iscph  22893  tchval  22940  limcfval  23559  dvfval  23584  eldv  23585  mdegfval  23743  mdegmullem  23759  mdegpropd  23765  coe1mul3  23780  ig1pval  23853  taylfval  24034  ishlg  25414  mirval  25467  ishpg  25568  lmif  25594  islmib  25596  vtxdgfval  26267  vtxdeqd  26276  grpoinvfval  27246  nmoofval  27487  eigvalfval  28626  ressnm  29460  ordtprsval  29770  ordtprsuni  29771  ordtrestNEW  29773  indv  29880  ofcfval  29965  ofcfval3  29969  omsval  30160  sitgval  30199  issibf  30200  sitgfval  30208  signstfv  30444  cvmliftlem5  31014  cvmliftlem15  31023  mvrsval  31145  mrsubffval  31147  elmrsubrn  31160  msubffval  31163  mvhfval  31173  msrfval  31177  fwddifval  31946  fwddifnval  31947  tailfval  32044  cureq  33052  lsatset  33792  lkrfval  33889  pmapfval  34557  pclfvalN  34690  polfvalN  34705  watfvalN  34793  ldilfset  34909  ltrnfset  34918  dilfsetN  34954  trnfsetN  34957  trlfset  34962  trlset  34963  tgrpfset  35547  tendofset  35561  erngfset  35602  erngset  35603  erngfset-rN  35610  erngset-rN  35611  dvafset  35807  diaffval  35834  diafval  35835  dvhfset  35884  docaffvalN  35925  docafvalN  35926  djaffvalN  35937  dibffval  35944  dibfval  35945  dicffval  35978  dicfval  35979  dihffval  36034  dochffval  36153  dochfval  36154  djhffval  36200  lcdfval  36392  mapdffval  36430  mapdfval  36431  hvmapffval  36562  hvmapfval  36563  hdmap1ffval  36600  hdmap1fval  36601  hdmapffval  36633  hdmapfval  36634  hgmapffval  36692  hgmapfval  36693  hlhilset  36741  hbtlem1  37209  hbtlem7  37211  rgspnval  37254  cytpval  37303  rfovd  37812  fsovd  37819  fsovcnvlem  37824  dssmapfvd  37828  ntrneibex  37888  ovnval  40088  hspmbllem2  40174  smflimsuplem1  40359  smflimsuplem7  40365  smflimsup  40367  ply1mulgsumlem3  41490  ply1mulgsumlem4  41491  ply1mulgsum  41492  lincval  41512  offval0  41613
  Copyright terms: Public domain W3C validator