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

Theorem ovmpoa 7288
 Description: Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
Hypotheses
Ref Expression
ovmpoga.1 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑅 = 𝑆)
ovmpoga.2 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
ovmpoa.4 𝑆 ∈ V
Assertion
Ref Expression
ovmpoa ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem ovmpoa
StepHypRef Expression
1 ovmpoa.4 . 2 𝑆 ∈ V
2 ovmpoga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑅 = 𝑆)
3 ovmpoga.2 . . 3 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
42, 3ovmpoga 7287 . 2 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
51, 4mp3an3 1447 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2112  Vcvv 3444  (class class class)co 7139   ∈ cmpo 7141 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-iota 6287  df-fun 6330  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144 This theorem is referenced by:  1st2val  7703  2nd2val  7704  cantnffval  9114  cantnfsuc  9121  fseqenlem1  9439  xaddval  12608  xmulval  12610  fzoval  13038  expval  13431  ccatfval  13920  splcl  14109  cshfn  14147  bpolylem  15397  ruclem1  15579  sadfval  15794  sadcp1  15797  smufval  15819  smupp1  15822  eucalgval2  15918  pcval  16174  pc0  16184  vdwapval  16302  pwsval  16754  xpsfval  16834  xpsval  16838  rescval  17092  isfunc  17129  isfull  17175  isfth  17179  natfval  17211  catcisolem  17361  xpchom  17425  1stfval  17436  2ndfval  17439  yonedalem3a  17519  yonedainv  17526  plusfval  17854  ismhm  17953  mulgval  18223  eqgfval  18323  isga  18416  subgga  18425  cayleylem1  18535  sylow1lem2  18719  isslw  18728  sylow2blem1  18740  sylow3lem1  18747  sylow3lem6  18752  frgpuptinv  18892  frgpup2  18897  isrhm  19472  scafval  19649  islmhm  19795  xrsdsval  20138  ipfval  20341  dsmmval  20426  psrmulfval  20626  mplval  20669  ltbval  20714  mpfrcl  20760  evlsval  20761  evlval  20770  mhpfval  20794  matval  21019  submafval  21187  mdetfval  21194  minmar1fval  21254  txval  22172  xkoval  22195  hmeofval  22366  flffval  22597  qustgplem  22729  dscmet  23182  dscopn  23183  tngval  23248  nmofval  23323  nghmfval  23331  isnmhm  23355  htpyco1  23586  htpycc  23588  phtpycc  23599  reparphti  23605  pcoval  23619  pcohtpylem  23627  pcorevlem  23634  dyadval  24199  itg1addlem3  24305  itg1addlem4  24306  mbfi1fseqlem3  24324  mbfi1fseqlem4  24325  mbfi1fseqlem5  24326  mbfi1fseqlem6  24327  mdegfval  24666  quotval  24891  elqaalem2  24919  cxpval  25258  cxpcn3  25340  angval  25390  sgmval  25730  lgsval  25888  wwlksn  27626  wspthsn  27637  rusgrnumwwlklem  27759  clwwlkn  27814  2clwwlk  28135  numclwwlkovh0  28160  numclwwlkovq  28162  shsval  29098  sshjval  29136  faeval  31613  txsconnlem  32595  cvxsconn  32598  iscvm  32614  cvmliftlem5  32644  rngohomval  35395  rngoisoval  35408  rmxfval  39832  rmyfval  39833  mendplusg  40117  mendvsca  40122  mnringvald  40908  addrval  41157  subrval  41158  mulvval  41159  sigarval  43451  ismgmhm  44390  dmatALTval  44796  naryfval  45029
 Copyright terms: Public domain W3C validator