Theorem ovmpoa 7513

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

Step	Hyp	Ref	Expression
1		ovmpoa.4	. 2 ⊢ 𝑆 ∈ V
2		ovmpoga.1	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
3		ovmpoga.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
4	2, 3	ovmpoga 7512	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
5	1, 4	mp3an3 1452	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3440  (class class class)co 7358   ∈ cmpo 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363

This theorem is referenced by:  ovmpot  7519  1st2val  7961  2nd2val  7962  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  cantnffval  9572  cantnfsuc  9579  fseqenlem1  9934  xaddval  13138  xmulval  13140  fzoval  13576  expval  13986  ccatfval  14496  splcl  14675  cshfn  14713  bpolylem  15971  ruclem1  16156  sadfval  16379  sadcp1  16382  smufval  16404  smupp1  16407  eucalgval2  16508  pcval  16772  pc0  16782  vdwapval  16901  pwsval  17406  xpsfval  17487  xpsval  17491  rescval  17751  isfunc  17788  isfull  17836  isfth  17840  natfval  17873  catcisolem  18034  xpchom  18103  1stfval  18114  2ndfval  18117  yonedalem3a  18197  yonedainv  18204  plusfval  18572  ismgmhm  18621  ismhm  18710  mulgval  19001  eqgfval  19105  isghm  19144  isga  19220  subgga  19229  cayleylem1  19341  sylow1lem2  19528  isslw  19537  sylow2blem1  19549  sylow3lem1  19556  sylow3lem6  19561  frgpuptinv  19700  frgpup2  19705  isrhm  20414  scafval  20832  islmhm  20979  xrsdsval  21365  ipfval  21604  dsmmval  21689  psrmulfval  21899  mplval  21944  ltbval  21998  mpfrcl  22040  evlsval  22041  evlval  22055  mhpfval  22081  matval  22355  submafval  22523  mdetfval  22530  minmar1fval  22590  txval  23508  xkoval  23531  hmeofval  23702  flffval  23933  qustgplem  24065  dscmet  24516  dscopn  24517  tngval  24583  nmofval  24658  nghmfval  24666  isnmhm  24690  htpyco1  24933  htpycc  24935  phtpycc  24946  reparphti  24952  reparphtiOLD  24953  pcoval  24967  pcohtpylem  24975  pcorevlem  24982  dyadval  25549  itg1addlem3  25655  itg1addlem4  25656  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  mdegfval  26023  quotval  26256  elqaalem2  26284  cxpval  26629  cxpcn3  26714  angval  26767  sgmval  27108  lgsval  27268  wwlksn  29910  wspthsn  29921  rusgrnumwwlklem  30046  clwwlkn  30101  2clwwlk  30422  numclwwlkovh0  30447  numclwwlkovq  30449  shsval  31387  sshjval  31425  faeval  34403  txsconnlem  35434  cvxsconn  35437  iscvm  35453  cvmliftlem5  35483  mpomulnzcnf  36493  rngohomval  38161  rngoisoval  38174  evlselv  42826  prjcrvfval  42870  rmxfval  43142  rmyfval  43143  mendplusg  43420  mendvsca  43425  mnringvald  44450  addrval  44702  subrval  44703  mulvval  44704  sigarval  47090  dmatALTval  48642  naryfval  48870  discsubc  49305  oppfvalg  49367  upfval  49417  setc1onsubc  49843  lmdfval  49890  cmdfval  49891