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

Theorem ovmpt2a 6433
Description: Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
Hypotheses
Ref Expression
ovmpt2ga.1
ovmpt2ga.2
ovmpt2a.4
Assertion
Ref Expression
ovmpt2a
Distinct variable groups:   , ,   , ,   , ,   , ,   ,S,

Proof of Theorem ovmpt2a
StepHypRef Expression
1 ovmpt2a.4 . 2
2 ovmpt2ga.1 . . 3
3 ovmpt2ga.2 . . 3
42, 3ovmpt2ga 6432 . 2
51, 4mp3an3 1313 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818   cvv 3109  (class class class)co 6296  e.cmpt2 6298
This theorem is referenced by:  1st2val  6826  2nd2val  6827  cantnffval  8101  cantnfsuc  8110  cantnfsucOLD  8140  fseqenlem1  8426  xaddval  11451  xmulval  11453  fzoval  11830  expval  12168  ccatfval  12592  splcl  12728  cshfn  12761  ruclem1  13964  sadfval  14102  sadcp1  14105  smufval  14127  smupp1  14130  eucalgval2  14210  pcval  14368  pc0  14378  vdwapval  14491  pwsval  14883  xpsfval  14964  xpsval  14969  rescval  15196  isfunc  15233  isfull  15279  isfth  15283  natfval  15315  catcisolem  15433  xpchom  15449  1stfval  15460  2ndfval  15463  yonedalem3a  15543  yonedainv  15550  plusfval  15878  ismhm  15968  mulgval  16144  eqgfval  16249  isga  16329  subgga  16338  cayleylem1  16437  sylow1lem2  16619  isslw  16628  sylow2blem1  16640  sylow3lem1  16647  sylow3lem6  16652  frgpuptinv  16789  frgpup2  16794  isrhm  17370  scafval  17531  islmhm  17673  psrmulfval  18038  mplval  18084  ltbval  18136  mpfrcl  18187  evlsval  18188  evlval  18193  xrsdsval  18462  ipfval  18684  dsmmval  18765  matval  18913  submafval  19081  mdetfval  19088  minmar1fval  19148  txval  20065  xkoval  20088  hmeofval  20259  flffval  20490  qustgplem  20619  dscmet  21093  dscopn  21094  tngval  21153  nmofval  21221  nghmfval  21229  isnmhm  21253  htpyco1  21478  htpycc  21480  phtpycc  21491  reparphti  21497  pcoval  21511  pcohtpylem  21519  pcorevlem  21526  dyadval  22001  itg1addlem3  22105  itg1addlem4  22106  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1fseqlem6  22127  mdegfval  22460  quotval  22688  elqaalem2  22716  cxpval  23045  cxpcn3  23122  angval  23133  sgmval  23416  lgsval  23575  clwwlknprop  24772  rusgranumwlklem2  24950  numclwwlkovf  25081  numclwwlkovg  25087  numclwwlkovq  25099  numclwwlkovh  25101  shsval  26230  sshjval  26268  faeval  28218  txsconlem  28685  cvxscon  28688  iscvm  28704  cvmliftlem5  28734  bpolylem  29810  rngohomval  30367  rngoisoval  30380  rmxfval  30840  rmyfval  30841  mendplusg  31135  mendvsca  31140  addrval  31375  subrval  31376  mulvval  31377  sigarval  32067  ismgmhm  32471  dmatALTval  33001
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-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301
  Copyright terms: Public domain W3C validator