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

Theorem mpteq12dv 5142
Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Drop ax-10 2136 while shortening its proof. (Revised by Steven Nguyen 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 nfv 1906 . 2 𝑥𝜑
2 mpteq12dv.1 . 2 (𝜑𝐴 = 𝐶)
3 mpteq12dv.2 . 2 (𝜑𝐵 = 𝐷)
41, 2, 3mpteq12df 5139 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cmpt 5137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-opab 5120  df-mpt 5138
This theorem is referenced by:  mpteq12i  5150  ovmpt3rab1  7392  offval  7405  offval3  7672  cantnffval  9114  cnfcomlem  9150  fseqenlem1  9438  dfac12lem1  9557  dfac12r  9560  ackbij2lem2  9650  ackbij2lem3  9651  r1om  9654  ccatfval  13913  swrdval  13993  revval  14110  odzval  16116  vdwpc  16304  restval  16688  prdsval  16716  imasval  16772  qusval  16803  mrcfval  16867  cidfval  16935  monfval  16990  ismon  16991  isepi  16998  idfuval  17134  resfval  17150  resfval2  17151  fucval  17216  homafval  17277  idafval  17305  prfval  17437  prf2fval  17439  curfval  17461  curfpropd  17471  hofval  17490  hof2fval  17493  yonedalem3a  17512  yonedalem4a  17513  yonedalem4c  17515  yonedainv  17519  lubfval  17576  glbfval  17589  ipoval  17752  grpinvfval  18080  grpinvfvalALT  18081  grpinvpropd  18112  mulgnn0gsum  18172  cntzfval  18388  pmtrfval  18507  psgnfval  18557  odfval  18589  odfvalALT  18590  sylow1lem2  18653  sylow1lem4  18655  sylow2blem1  18674  sylow3lem1  18681  sylow3lem2  18682  sylow3lem3  18683  sylow3lem6  18686  pj1fval  18749  vrgpfval  18821  gsum2dlem2  19020  gsum2d2  19023  dprdval  19054  dprd2dlem2  19091  dprd2dlem1  19092  dprd2da  19093  dprd2d2  19095  dpjfval  19106  srgbinom  19224  staffval  19547  lspfval  19674  lsppropd  19719  sraval  19877  aspval  20030  asclfval  20036  ressascl  20053  psrval  20070  psrass1lem  20085  psrmulval  20094  mvrfval  20128  opsrval  20183  mpfrcl  20226  evlsval  20227  selvffval  20257  coe1mul2  20365  cply1mul  20390  evls1fval  20410  evl1fval  20419  isphl  20700  ocvfval  20738  pjfval  20778  uvcfval  20856  mamufval  20924  mvmulfval  21079  marepvfval  21102  submafval  21116  mdetfval  21123  madufval  21174  minmar1fval  21183  mat2pmatfval  21259  cpm2mfval  21285  decpmatmullem  21307  decpmatmulsumfsupp  21309  pm2mpval  21331  pm2mpmhmlem1  21354  pm2mpmhmlem2  21355  chpmatfval  21366  ntrfval  21560  clsfval  21561  neifval  21635  lpfval  21674  ordtval  21725  ordtbas2  21727  ordtcnv  21737  ordtrest  21738  ordtrest2  21740  cnpfval  21770  kqval  22262  fmval  22479  fmf  22481  flffval  22525  fcfval  22569  cnextval  22597  tsmsval2  22665  nmfval  23125  nmpropd  23130  nmpropd2  23131  subgnm  23169  tngnm  23187  nmofval  23250  pi1xfrcnv  23588  iscph  23701  tcphval  23748  limcfval  24397  dvfval  24422  eldv  24423  mdegfval  24583  mdegmullem  24599  mdegpropd  24605  coe1mul3  24620  ig1pval  24693  taylfval  24874  ishlg  26315  mirval  26368  ishpg  26472  lmif  26498  islmib  26500  vtxdgfval  27176  vtxdeqd  27186  grpoinvfval  28226  nmoofval  28466  eigvalfval  29601  ressnm  30565  tocycval  30677  ordtprsval  31060  ordtprsuni  31061  ordtrestNEW  31063  indv  31170  ofcfval  31256  ofcfval3  31260  omsval  31450  sitgval  31489  issibf  31490  sitgfval  31498  signstfv  31732  cvmliftlem5  32433  cvmliftlem15  32442  mvrsval  32649  mrsubffval  32651  elmrsubrn  32664  msubffval  32667  mvhfval  32677  msrfval  32681  fwddifval  33520  fwddifnval  33521  tailfval  33617  bj-imdirval  34364  cureq  34749  lsatset  36006  lkrfval  36103  pmapfval  36772  pclfvalN  36905  polfvalN  36920  watfvalN  37008  ldilfset  37124  ltrnfset  37133  dilfsetN  37168  trnfsetN  37171  trlfset  37176  trlset  37177  tgrpfset  37760  tendofset  37774  erngfset  37815  erngset  37816  erngfset-rN  37823  erngset-rN  37824  dvafset  38020  diaffval  38046  diafval  38047  dvhfset  38096  docaffvalN  38137  docafvalN  38138  djaffvalN  38149  dibffval  38156  dibfval  38157  dicffval  38190  dicfval  38191  dihffval  38246  dochffval  38365  dochfval  38366  djhffval  38412  lcdfval  38604  mapdffval  38642  mapdfval  38643  hvmapffval  38774  hvmapfval  38775  hdmap1ffval  38811  hdmap1fval  38812  hdmapffval  38842  hdmapfval  38843  hgmapffval  38901  hgmapfval  38902  hlhilset  38950  hbtlem1  39601  hbtlem7  39603  rgspnval  39646  cytpval  39687  rfovd  40225  fsovd  40232  fsovcnvlem  40237  dssmapfvd  40241  ntrneibex  40301  ovnval  42700  hspmbllem2  42786  smflimsuplem1  42971  smflimsuplem3  42973  smflimsuplem7  42977  smflimsup  42979  ply1mulgsumlem3  44370  ply1mulgsumlem4  44371  ply1mulgsum  44372  lincval  44392
  Copyright terms: Public domain W3C validator