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

Theorem mpteq12dv 4885
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 472 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
41, 3mpteq12dva 4884 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  cmpt 4881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ral 3055  df-opab 4865  df-mpt 4882
This theorem is referenced by:  mpteq12i  4894  ovmpt3rab1  7056  offval  7069  offval3  7327  cantnffval  8733  cnfcomlem  8769  fseqenlem1  9037  dfac12lem1  9157  dfac12r  9160  ackbij2lem2  9254  ackbij2lem3  9255  r1om  9258  ccatfval  13545  swrdval  13616  revval  13709  odzval  15698  vdwpc  15886  restval  16289  prdsval  16317  imasval  16373  qusval  16404  mrcfval  16470  cidfval  16538  monfval  16593  ismon  16594  isepi  16601  idfuval  16737  resfval  16753  resfval2  16754  fucval  16819  homafval  16880  idafval  16908  prfval  17040  prf2fval  17042  curfval  17064  curfpropd  17074  hofval  17093  hof2fval  17096  yonedalem3a  17115  yonedalem4a  17116  yonedalem4c  17118  yonedainv  17122  lubfval  17179  glbfval  17192  ipoval  17355  grpinvfval  17661  grpinvpropd  17691  cntzfval  17953  pmtrfval  18070  psgnfval  18120  odfval  18152  sylow1lem2  18214  sylow1lem4  18216  sylow2blem1  18235  sylow3lem1  18242  sylow3lem2  18243  sylow3lem3  18244  sylow3lem6  18247  pj1fval  18307  vrgpfval  18379  gsum2dlem2  18570  gsum2d2  18573  dprdval  18602  dprd2dlem2  18639  dprd2dlem1  18640  dprd2da  18641  dprd2d2  18643  dpjfval  18654  srgbinom  18745  staffval  19049  lspfval  19175  lsppropd  19220  sraval  19378  aspval  19530  asclfval  19536  ressascl  19546  psrval  19564  psrass1lem  19579  psrmulval  19588  mvrfval  19622  opsrval  19676  mpfrcl  19720  evlsval  19721  coe1mul2  19841  cply1mul  19866  evls1fval  19886  evl1fval  19894  isphl  20175  ocvfval  20212  pjfval  20252  uvcfval  20325  mamufval  20393  mvmulfval  20550  marepvfval  20573  submafval  20587  mdetfval  20594  madufval  20645  minmar1fval  20654  mat2pmatfval  20730  cpm2mfval  20756  decpmatmullem  20778  decpmatmulsumfsupp  20780  pm2mpval  20802  pm2mpmhmlem1  20825  pm2mpmhmlem2  20826  chpmatfval  20837  ntrfval  21030  clsfval  21031  neifval  21105  lpfval  21144  ordtval  21195  ordtbas2  21197  ordtcnv  21207  ordtrest  21208  ordtrest2  21210  cnpfval  21240  kqval  21731  fmval  21948  fmf  21950  flffval  21994  fcfval  22038  cnextval  22066  tsmsval2  22134  nmfval  22594  nmpropd  22599  nmpropd2  22600  subgnm  22638  tngnm  22656  nmofval  22719  pi1xfrcnv  23057  iscph  23170  tchval  23217  limcfval  23835  dvfval  23860  eldv  23861  mdegfval  24021  mdegmullem  24037  mdegpropd  24043  coe1mul3  24058  ig1pval  24131  taylfval  24312  ishlg  25696  mirval  25749  ishpg  25850  lmif  25876  islmib  25878  vtxdgfval  26573  vtxdeqd  26583  grpoinvfval  27685  nmoofval  27926  eigvalfval  29065  ressnm  29960  ordtprsval  30273  ordtprsuni  30274  ordtrestNEW  30276  indv  30383  ofcfval  30469  ofcfval3  30473  omsval  30664  sitgval  30703  issibf  30704  sitgfval  30712  signstfv  30949  cvmliftlem5  31578  cvmliftlem15  31587  mvrsval  31709  mrsubffval  31711  elmrsubrn  31724  msubffval  31727  mvhfval  31737  msrfval  31741  fwddifval  32575  fwddifnval  32576  tailfval  32673  cureq  33698  lsatset  34780  lkrfval  34877  pmapfval  35545  pclfvalN  35678  polfvalN  35693  watfvalN  35781  ldilfset  35897  ltrnfset  35906  dilfsetN  35942  trnfsetN  35945  trlfset  35950  trlset  35951  tgrpfset  36534  tendofset  36548  erngfset  36589  erngset  36590  erngfset-rN  36597  erngset-rN  36598  dvafset  36794  diaffval  36821  diafval  36822  dvhfset  36871  docaffvalN  36912  docafvalN  36913  djaffvalN  36924  dibffval  36931  dibfval  36932  dicffval  36965  dicfval  36966  dihffval  37021  dochffval  37140  dochfval  37141  djhffval  37187  lcdfval  37379  mapdffval  37417  mapdfval  37418  hvmapffval  37549  hvmapfval  37550  hdmap1ffval  37587  hdmap1fval  37588  hdmapffval  37620  hdmapfval  37621  hgmapffval  37679  hgmapfval  37680  hlhilset  37728  hbtlem1  38195  hbtlem7  38197  rgspnval  38240  cytpval  38289  rfovd  38797  fsovd  38804  fsovcnvlem  38809  dssmapfvd  38813  ntrneibex  38873  ovnval  41261  hspmbllem2  41347  smflimsuplem1  41532  smflimsuplem7  41538  smflimsup  41540  ply1mulgsumlem3  42686  ply1mulgsumlem4  42687  ply1mulgsum  42688  lincval  42708  offval0  42809
  Copyright terms: Public domain W3C validator