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

Theorem mpteq12dv 5200
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 2138, ax-12 2172. (Revised by SN and Gino Giotto, 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 482 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
41, 3mpteq12dva 5198 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  cmpt 5192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5172  df-mpt 5193
This theorem is referenced by:  mpteq1  5202  mpteq1i  5205  mpteq12i  5215  ovmpt3rab1  7615  offval  7630  offval3  7919  cantnffval  9607  cnfcomlem  9643  fseqenlem1  9968  dfac12lem1  10087  dfac12r  10090  ackbij2lem2  10184  ackbij2lem3  10185  r1om  10188  ccatfval  14470  swrdval  14540  revval  14657  odzval  16671  vdwpc  16860  restval  17316  prdsval  17345  imasval  17401  qusval  17432  mrcfval  17496  cidfval  17564  monfval  17623  ismon  17624  isepi  17631  idfuval  17770  resfval  17786  resfval2  17787  fucval  17854  homafval  17923  idafval  17951  prfval  18095  prf2fval  18097  curfval  18120  curfpropd  18130  hofval  18149  hof2fval  18152  yonedalem3a  18171  yonedalem4a  18172  yonedalem4c  18174  yonedainv  18178  lubfval  18247  glbfval  18260  ipoval  18427  grpinvfval  18797  grpinvfvalALT  18798  grpinvpropd  18830  mulgnn0gsum  18890  cntzfval  19108  pmtrfval  19240  psgnfval  19290  odfval  19322  odfvalALT  19323  sylow1lem2  19389  sylow1lem4  19391  sylow2blem1  19410  sylow3lem1  19417  sylow3lem2  19418  sylow3lem3  19419  sylow3lem6  19422  pj1fval  19484  vrgpfval  19556  gsum2dlem2  19756  gsum2d2  19759  dprdval  19790  dprd2dlem2  19827  dprd2dlem1  19828  dprd2da  19829  dprd2d2  19831  dpjfval  19842  srgbinom  19970  staffval  20349  lspfval  20478  lsppropd  20523  sraval  20682  isphl  21055  ocvfval  21093  pjfval  21135  uvcfval  21213  aspval  21299  asclfval  21305  ressascl  21322  psrval  21340  psrass1lemOLD  21365  psrass1lem  21368  psrmulval  21377  mvrfval  21412  opsrval  21470  mpfrcl  21518  evlsval  21519  selvffval  21549  mhpmulcl  21562  coe1mul2  21663  cply1mul  21688  evls1fval  21708  evl1fval  21717  mamufval  21757  mvmulfval  21914  marepvfval  21937  submafval  21951  mdetfval  21958  madufval  22009  minmar1fval  22018  mat2pmatfval  22095  cpm2mfval  22121  decpmatmullem  22143  decpmatmulsumfsupp  22145  pm2mpval  22167  pm2mpmhmlem1  22190  pm2mpmhmlem2  22191  chpmatfval  22202  ntrfval  22398  clsfval  22399  neifval  22473  lpfval  22512  ordtval  22563  ordtbas2  22565  ordtcnv  22575  ordtrest  22576  ordtrest2  22578  cnpfval  22608  kqval  23100  fmval  23317  fmf  23319  flffval  23363  fcfval  23407  cnextval  23435  tsmsval2  23504  nmfval  23967  nmpropd  23973  nmpropd2  23974  subgnm  24012  tngnm  24038  nmofval  24101  pi1xfrcnv  24443  iscph  24557  tcphval  24605  limcfval  25259  dvfval  25284  eldv  25285  mdegfval  25450  mdegmullem  25466  mdegpropd  25472  coe1mul3  25487  ig1pval  25560  taylfval  25741  ishlg  27593  mirval  27646  ishpg  27750  lmif  27776  islmib  27778  vtxdgfval  28464  vtxdeqd  28474  grpoinvfval  29513  nmoofval  29753  eigvalfval  30888  ressnm  31874  tocycval  32013  idlsrgval  32300  minplyval  32436  ordtprsval  32563  ordtprsuni  32564  ordtrestNEW  32566  indv  32675  ofcfval  32761  ofcfval3  32765  omsval  32957  sitgval  32996  issibf  32997  sitgfval  33005  signstfv  33239  cvmliftlem5  33947  cvmliftlem15  33956  mvrsval  34163  mrsubffval  34165  elmrsubrn  34178  msubffval  34181  mvhfval  34191  msrfval  34195  fwddifval  34800  fwddifnval  34801  tailfval  34897  bj-imdirvallem  35701  bj-endval  35836  cureq  36104  lsatset  37502  lkrfval  37599  pmapfval  38269  pclfvalN  38402  polfvalN  38417  watfvalN  38505  ldilfset  38621  ltrnfset  38630  dilfsetN  38665  trnfsetN  38668  trlfset  38673  trlset  38674  tgrpfset  39257  tendofset  39271  erngfset  39312  erngset  39313  erngfset-rN  39320  erngset-rN  39321  dvafset  39517  diaffval  39543  diafval  39544  dvhfset  39593  docaffvalN  39634  docafvalN  39635  djaffvalN  39646  dibffval  39653  dibfval  39654  dicffval  39687  dicfval  39688  dihffval  39743  dochffval  39862  dochfval  39863  djhffval  39909  lcdfval  40101  mapdffval  40139  mapdfval  40140  hvmapffval  40271  hvmapfval  40272  hdmap1ffval  40308  hdmap1fval  40309  hdmapffval  40339  hdmapfval  40340  hgmapffval  40398  hgmapfval  40399  hlhilset  40447  prjcrvfval  41016  hbtlem1  41497  hbtlem7  41499  rgspnval  41542  cytpval  41583  rfovd  42365  fsovd  42372  fsovcnvlem  42377  dssmapfvd  42381  ntrneibex  42437  mnringvald  42580  ovnval  44872  hspmbllem2  44958  smflimsuplem1  45151  smflimsuplem3  45153  smflimsuplem7  45157  smflimsup  45159  ply1mulgsumlem3  46559  ply1mulgsumlem4  46560  ply1mulgsum  46561  lincval  46580
  Copyright terms: Public domain W3C validator