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

Theorem mpteq12dv 4530
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:   ,

Proof of Theorem mpteq12dv
StepHypRef Expression
1 mpteq12dv.1 . 2
2 mpteq12dv.2 . . 3
32adantr 465 . 2
41, 3mpteq12dva 4529 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  e.cmpt 4510
This theorem is referenced by:  mpteq12i  4536  ovmpt3rab1  6534  offval  6547  offval3  6794  cantnffval  8101  cnfcomlem  8164  cnfcomlemOLD  8172  fseqenlem1  8426  dfac12lem1  8544  dfac12r  8547  ackbij2lem2  8641  ackbij2lem3  8642  r1om  8645  ccatfval  12592  swrdval  12644  revval  12734  odzval  14318  vdwpc  14498  restval  14824  prdsval  14852  imasval  14908  qusval  14939  mrcfval  15005  cidfval  15073  monfval  15127  ismon  15128  isepi  15135  idfuval  15245  resfval  15261  resfval2  15262  fucval  15327  homafval  15356  idafval  15384  prfval  15468  prf2fval  15470  curfval  15492  curfpropd  15502  hofval  15521  hof2fval  15524  yonedalem3a  15543  yonedalem4a  15544  yonedalem4c  15546  yonedainv  15550  lubfval  15608  glbfval  15621  ipoval  15784  grpinvfval  16088  grpinvpropd  16113  cntzfval  16358  pmtrfval  16475  psgnfval  16525  odfval  16557  sylow1lem2  16619  sylow1lem4  16621  sylow2blem1  16640  sylow3lem1  16647  sylow3lem2  16648  sylow3lem3  16649  sylow3lem6  16652  pj1fval  16712  vrgpfval  16784  gsum2dlem2  16998  gsum2dOLD  17000  gsum2d2  17002  dprdval  17034  dprdvalOLD  17036  dprd2dlem2  17089  dprd2dlem1  17090  dprd2da  17091  dprd2d2  17093  dpjfval  17104  srgbinom  17196  staffval  17496  lspfval  17619  lsppropd  17664  sraval  17822  aspval  17977  asclfval  17983  ressascl  17993  psrval  18011  psrass1lem  18029  psrmulval  18039  mvrfval  18076  opsrval  18139  mpfrcl  18187  evlsval  18188  coe1mul2  18310  cply1mul  18335  evls1fval  18356  evl1fval  18364  isphl  18663  ocvfval  18697  pjfval  18737  uvcfval  18815  mamufval  18887  mvmulfval  19044  marepvfval  19067  submafval  19081  mdetfval  19088  madufval  19139  minmar1fval  19148  mat2pmatfval  19224  cpm2mfval  19250  decpmatmullem  19272  decpmatmulsumfsupp  19274  pm2mpval  19296  pm2mpmhmlem1  19319  pm2mpmhmlem2  19320  chpmatfval  19331  ntrfval  19525  clsfval  19526  neifval  19600  lpfval  19639  ordtval  19690  ordtbas2  19692  ordtcnv  19702  ordtrest  19703  ordtrest2  19705  cnpfval  19735  kqval  20227  fmval  20444  fmf  20446  flffval  20490  fcfval  20534  cnextval  20561  tsmsval2  20628  nmfval  21109  nmpropd  21114  nmpropd2  21115  subgnm  21147  tngnm  21165  nmofval  21221  pi1xfrcnv  21557  iscph  21617  tchval  21661  limcfval  22276  dvfval  22301  eldv  22302  mdegfval  22460  mdegmullem  22478  mdegpropd  22484  coe1mul3  22500  ig1pval  22573  taylfval  22754  mirval  24036  ishpg  24128  lmif  24151  islmib  24153  vdgrfval  24895  grpoinvfval  25226  nmoofval  25677  eigvalfval  26816  ressnm  27639  ordtprsval  27900  ordtprsuni  27901  ordtrestNEW  27903  indv  28026  ofcfval  28097  ofcfval3  28101  omsval  28264  sitgval  28274  issibf  28275  sitgfval  28283  signstfv  28520  cvmliftlem5  28734  cvmliftlem15  28743  mvrsval  28865  mrsubffval  28867  elmrsubrn  28880  msubffval  28883  mvhfval  28893  msrfval  28897  tailfval  30190  hbtlem1  31072  hbtlem7  31074  rgspnval  31117  cytpval  31169  ply1mulgsumlem3  32988  ply1mulgsumlem4  32989  ply1mulgsum  32990  lincval  33010  lsatset  34715  lkrfval  34812  pmapfval  35480  pclfvalN  35613  polfvalN  35628  watfvalN  35716  ldilfset  35832  ltrnfset  35841  dilfsetN  35877  trnfsetN  35880  trlfset  35885  trlset  35886  tgrpfset  36470  tendofset  36484  erngfset  36525  erngset  36526  erngfset-rN  36533  erngset-rN  36534  dvafset  36730  diaffval  36757  diafval  36758  dvhfset  36807  docaffvalN  36848  docafvalN  36849  djaffvalN  36860  dibffval  36867  dibfval  36868  dicffval  36901  dicfval  36902  dihffval  36957  dochffval  37076  dochfval  37077  djhffval  37123  lcdfval  37315  mapdffval  37353  mapdfval  37354  hvmapffval  37485  hvmapfval  37486  hdmap1ffval  37523  hdmap1fval  37524  hdmapffval  37556  hdmapfval  37557  hgmapffval  37615  hgmapfval  37616  hlhilset  37664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-opab 4511  df-mpt 4512
  Copyright terms: Public domain W3C validator