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

Theorem ovmpt2a 6958
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 6957 . 2 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
51, 4mp3an3 1562 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2140  Vcvv 3341  (class class class)co 6815  cmpt2 6817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pr 5056
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-iota 6013  df-fun 6052  df-fv 6058  df-ov 6818  df-oprab 6819  df-mpt2 6820
This theorem is referenced by:  1st2val  7363  2nd2val  7364  cantnffval  8736  cantnfsuc  8743  fseqenlem1  9058  xaddval  12268  xmulval  12270  fzoval  12686  expval  13077  ccatfval  13566  splcl  13724  cshfn  13757  bpolylem  14999  ruclem1  15180  sadfval  15397  sadcp1  15400  smufval  15422  smupp1  15425  eucalgval2  15517  pcval  15772  pc0  15782  vdwapval  15900  pwsval  16369  xpsfval  16450  xpsval  16455  rescval  16709  isfunc  16746  isfull  16792  isfth  16796  natfval  16828  catcisolem  16978  xpchom  17042  1stfval  17053  2ndfval  17056  yonedalem3a  17136  yonedainv  17143  plusfval  17470  ismhm  17559  mulgval  17765  eqgfval  17864  isga  17945  subgga  17954  cayleylem1  18053  sylow1lem2  18235  isslw  18244  sylow2blem1  18256  sylow3lem1  18263  sylow3lem6  18268  frgpuptinv  18405  frgpup2  18410  isrhm  18944  scafval  19105  islmhm  19250  psrmulfval  19608  mplval  19651  ltbval  19694  mpfrcl  19741  evlsval  19742  evlval  19747  xrsdsval  20013  ipfval  20217  dsmmval  20301  matval  20440  submafval  20608  mdetfval  20615  minmar1fval  20675  txval  21590  xkoval  21613  hmeofval  21784  flffval  22015  qustgplem  22146  dscmet  22599  dscopn  22600  tngval  22665  nmofval  22740  nghmfval  22748  isnmhm  22772  htpyco1  22999  htpycc  23001  phtpycc  23012  reparphti  23018  pcoval  23032  pcohtpylem  23040  pcorevlem  23047  dyadval  23581  itg1addlem3  23685  itg1addlem4  23686  mbfi1fseqlem3  23704  mbfi1fseqlem4  23705  mbfi1fseqlem5  23706  mbfi1fseqlem6  23707  mdegfval  24042  quotval  24267  elqaalem2  24295  cxpval  24631  cxpcn3  24710  angval  24752  sgmval  25089  lgsval  25247  wspthsn  26974  rusgrnumwwlklem  27114  clwwlkn  27173  2clwwlk  27526  numclwwlkovgOLD  27530  numclwwlkovh0  27555  numclwwlkovq  27557  numclwwlkovhOLD  27565  shsval  28502  sshjval  28540  faeval  30640  txsconnlem  31551  cvxsconn  31554  iscvm  31570  cvmliftlem5  31600  rngohomval  34095  rngoisoval  34108  rmxfval  37989  rmyfval  37990  mendplusg  38277  mendvsca  38282  addrval  39191  subrval  39192  mulvval  39193  sigarval  41564  ismgmhm  42312  dmatALTval  42718
  Copyright terms: Public domain W3C validator