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

Theorem mpteq12dv 5240
Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Remove dependency on ax-10 2129, ax-12 2166. (Revised by SN and GG, 1-Dec-2023.)
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 479 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
41, 3mpteq12dva 5238 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wcel 2098  cmpt 5232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-opab 5212  df-mpt 5233
This theorem is referenced by:  mpteq1  5242  mpteq1i  5245  mpteq12i  5255  ovmpt3rab1  7679  offval  7694  offval3  7987  cantnffval  9688  cnfcomlem  9724  fseqenlem1  10049  dfac12lem1  10168  dfac12r  10171  ackbij2lem2  10265  ackbij2lem3  10266  r1om  10269  ccatfval  14559  swrdval  14629  revval  14746  odzval  16763  vdwpc  16952  restval  17411  prdsval  17440  imasval  17496  qusval  17527  mrcfval  17591  cidfval  17659  monfval  17718  ismon  17719  isepi  17726  idfuval  17865  resfval  17881  resfval2  17882  fucval  17952  homafval  18021  idafval  18049  prfval  18193  prf2fval  18195  curfval  18218  curfpropd  18228  hofval  18247  hof2fval  18250  yonedalem3a  18269  yonedalem4a  18270  yonedalem4c  18272  yonedainv  18276  lubfval  18345  glbfval  18358  ipoval  18525  grpinvfval  18943  grpinvfvalALT  18944  grpinvpropd  18979  mulgnn0gsum  19043  cntzfval  19283  pmtrfval  19417  psgnfval  19467  odfval  19499  odfvalALT  19500  sylow1lem2  19566  sylow1lem4  19568  sylow2blem1  19587  sylow3lem1  19594  sylow3lem2  19595  sylow3lem3  19596  sylow3lem6  19599  pj1fval  19661  vrgpfval  19733  gsum2dlem2  19938  gsum2d2  19941  dprdval  19972  dprd2dlem2  20009  dprd2dlem1  20010  dprd2da  20011  dprd2d2  20013  dpjfval  20024  srgbinom  20183  staffval  20739  lspfval  20869  lsppropd  20915  sraval  21072  isphl  21577  ocvfval  21615  pjfval  21657  uvcfval  21735  aspval  21823  asclfval  21829  ressascl  21846  psrval  21865  psrass1lemOLD  21891  psrass1lem  21894  psrmulval  21906  mvrfval  21943  opsrval  22006  mpfrcl  22053  evlsval  22054  selvffval  22081  mhpmulcl  22096  psdffval  22104  coe1mul2  22213  cply1mul  22240  evls1fval  22263  evl1fval  22272  evl1maprhm  22323  mamufval  22336  mvmulfval  22488  marepvfval  22511  submafval  22525  mdetfval  22532  madufval  22583  minmar1fval  22592  mat2pmatfval  22669  cpm2mfval  22695  decpmatmullem  22717  decpmatmulsumfsupp  22719  pm2mpval  22741  pm2mpmhmlem1  22764  pm2mpmhmlem2  22765  chpmatfval  22776  ntrfval  22972  clsfval  22973  neifval  23047  lpfval  23086  ordtval  23137  ordtbas2  23139  ordtcnv  23149  ordtrest  23150  ordtrest2  23152  cnpfval  23182  kqval  23674  fmval  23891  fmf  23893  flffval  23937  fcfval  23981  cnextval  24009  tsmsval2  24078  nmfval  24541  nmpropd  24547  nmpropd2  24548  subgnm  24586  tngnm  24612  nmofval  24675  pi1xfrcnv  25028  iscph  25142  tcphval  25190  limcfval  25845  dvfval  25870  eldv  25871  mdegfval  26042  mdegmullem  26058  mdegpropd  26064  coe1mul3  26079  ig1pval  26155  taylfval  26338  ishlg  28478  mirval  28531  ishpg  28635  lmif  28661  islmib  28663  vtxdgfval  29353  vtxdeqd  29363  grpoinvfval  30404  nmoofval  30644  eigvalfval  31779  ressnm  32774  tocycval  32921  idlsrgval  33315  minplyval  33507  ordtprsval  33650  ordtprsuni  33651  ordtrestNEW  33653  indv  33762  ofcfval  33848  ofcfval3  33852  omsval  34044  sitgval  34083  issibf  34084  sitgfval  34092  signstfv  34326  cvmliftlem5  35030  cvmliftlem15  35039  mvrsval  35246  mrsubffval  35248  elmrsubrn  35261  msubffval  35264  mvhfval  35274  msrfval  35278  fwddifval  35889  fwddifnval  35890  tailfval  35987  bj-imdirvallem  36790  bj-endval  36925  cureq  37200  lsatset  38592  lkrfval  38689  pmapfval  39359  pclfvalN  39492  polfvalN  39507  watfvalN  39595  ldilfset  39711  ltrnfset  39720  dilfsetN  39755  trnfsetN  39758  trlfset  39763  trlset  39764  tgrpfset  40347  tendofset  40361  erngfset  40402  erngset  40403  erngfset-rN  40410  erngset-rN  40411  dvafset  40607  diaffval  40633  diafval  40634  dvhfset  40683  docaffvalN  40724  docafvalN  40725  djaffvalN  40736  dibffval  40743  dibfval  40744  dicffval  40777  dicfval  40778  dihffval  40833  dochffval  40952  dochfval  40953  djhffval  40999  lcdfval  41191  mapdffval  41229  mapdfval  41230  hvmapffval  41361  hvmapfval  41362  hdmap1ffval  41398  hdmap1fval  41399  hdmapffval  41429  hdmapfval  41430  hgmapffval  41488  hgmapfval  41489  hlhilset  41537  prjcrvfval  42190  hbtlem1  42689  hbtlem7  42691  rgspnval  42734  cytpval  42772  rfovd  43573  fsovd  43580  fsovcnvlem  43585  dssmapfvd  43589  ntrneibex  43645  mnringvald  43787  ovnval  46067  hspmbllem2  46153  smflimsuplem1  46346  smflimsuplem3  46348  smflimsuplem7  46352  smflimsup  46354  ply1mulgsumlem3  47642  ply1mulgsumlem4  47643  ply1mulgsum  47644  lincval  47663
  Copyright terms: Public domain W3C validator