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

Theorem ovmpt2a 6663
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 𝑆 ∈ V
Assertion
Ref Expression
ovmpt2a ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem ovmpt2a
StepHypRef Expression
1 ovmpt2a.4 . 2 𝑆 ∈ V
2 ovmpt2ga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑅 = 𝑆)
3 ovmpt2ga.2 . . 3 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
42, 3ovmpt2ga 6662 . 2 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
51, 4mp3an3 1404 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1975  Vcvv 3168  (class class class)co 6523  cmpt2 6525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-sbc 3398  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-iota 5750  df-fun 5788  df-fv 5794  df-ov 6526  df-oprab 6527  df-mpt2 6528
This theorem is referenced by:  1st2val  7058  2nd2val  7059  cantnffval  8416  cantnfsuc  8423  fseqenlem1  8703  xaddval  11883  xmulval  11885  fzoval  12291  expval  12675  ccatfval  13153  splcl  13296  cshfn  13329  bpolylem  14560  ruclem1  14741  sadfval  14954  sadcp1  14957  smufval  14979  smupp1  14982  eucalgval2  15074  pcval  15329  pc0  15339  vdwapval  15457  pwsval  15911  xpsfval  15992  xpsval  15997  rescval  16252  isfunc  16289  isfull  16335  isfth  16339  natfval  16371  catcisolem  16521  xpchom  16585  1stfval  16596  2ndfval  16599  yonedalem3a  16679  yonedainv  16686  plusfval  17013  ismhm  17102  mulgval  17308  eqgfval  17407  isga  17489  subgga  17498  cayleylem1  17597  sylow1lem2  17779  isslw  17788  sylow2blem1  17800  sylow3lem1  17807  sylow3lem6  17812  frgpuptinv  17949  frgpup2  17954  isrhm  18486  scafval  18647  islmhm  18790  psrmulfval  19148  mplval  19191  ltbval  19234  mpfrcl  19281  evlsval  19282  evlval  19287  xrsdsval  19551  ipfval  19754  dsmmval  19835  matval  19974  submafval  20142  mdetfval  20149  minmar1fval  20209  txval  21115  xkoval  21138  hmeofval  21309  flffval  21541  qustgplem  21672  dscmet  22124  dscopn  22125  tngval  22187  nmofval  22256  nghmfval  22264  isnmhm  22288  htpyco1  22512  htpycc  22514  phtpycc  22525  reparphti  22532  pcoval  22546  pcohtpylem  22554  pcorevlem  22561  dyadval  23079  itg1addlem3  23184  itg1addlem4  23185  mbfi1fseqlem3  23203  mbfi1fseqlem4  23204  mbfi1fseqlem5  23205  mbfi1fseqlem6  23206  mdegfval  23539  quotval  23764  elqaalem2  23792  cxpval  24123  cxpcn3  24202  angval  24244  sgmval  24581  lgsval  24739  clwwlknprop  26062  rusgranumwlklem2  26239  numclwwlkovf  26370  numclwwlkovg  26376  numclwwlkovq  26388  numclwwlkovh  26390  shsval  27357  sshjval  27395  faeval  29438  txsconlem  30278  cvxscon  30281  iscvm  30297  cvmliftlem5  30327  rngohomval  32732  rngoisoval  32745  rmxfval  36285  rmyfval  36286  mendplusg  36574  mendvsca  36579  addrval  37490  subrval  37491  mulvval  37492  sigarval  39488  wspthsn  41044  rusgrnumwwlklem  41171  av-numclwwlkovf  41509  av-numclwwlkovg  41516  av-numclwwlkovq  41527  av-numclwwlkovh  41529  ismgmhm  41571  dmatALTval  41981
  Copyright terms: Public domain W3C validator