Theorem ovmpoa 7523

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 7522	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
5	1, 4	mp3an3 1453	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442  (class class class)co 7368   ∈ cmpo 7370

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373

This theorem is referenced by:  ovmpot  7529  1st2val  7971  2nd2val  7972  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  cantnffval  9584  cantnfsuc  9591  fseqenlem1  9946  xaddval  13150  xmulval  13152  fzoval  13588  expval  13998  ccatfval  14508  splcl  14687  cshfn  14725  bpolylem  15983  ruclem1  16168  sadfval  16391  sadcp1  16394  smufval  16416  smupp1  16419  eucalgval2  16520  pcval  16784  pc0  16794  vdwapval  16913  pwsval  17418  xpsfval  17499  xpsval  17503  rescval  17763  isfunc  17800  isfull  17848  isfth  17852  natfval  17885  catcisolem  18046  xpchom  18115  1stfval  18126  2ndfval  18129  yonedalem3a  18209  yonedainv  18216  plusfval  18584  ismgmhm  18633  ismhm  18722  mulgval  19013  eqgfval  19117  isghm  19156  isga  19232  subgga  19241  cayleylem1  19353  sylow1lem2  19540  isslw  19549  sylow2blem1  19561  sylow3lem1  19568  sylow3lem6  19573  frgpuptinv  19712  frgpup2  19717  isrhm  20426  scafval  20844  islmhm  20991  xrsdsval  21377  ipfval  21616  dsmmval  21701  psrmulfval  21911  mplval  21956  ltbval  22010  mpfrcl  22052  evlsval  22053  evlval  22067  mhpfval  22093  matval  22367  submafval  22535  mdetfval  22542  minmar1fval  22602  txval  23520  xkoval  23543  hmeofval  23714  flffval  23945  qustgplem  24077  dscmet  24528  dscopn  24529  tngval  24595  nmofval  24670  nghmfval  24678  isnmhm  24702  htpyco1  24945  htpycc  24947  phtpycc  24958  reparphti  24964  reparphtiOLD  24965  pcoval  24979  pcohtpylem  24987  pcorevlem  24994  dyadval  25561  itg1addlem3  25667  itg1addlem4  25668  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  mdegfval  26035  quotval  26268  elqaalem2  26296  cxpval  26641  cxpcn3  26726  angval  26779  sgmval  27120  lgsval  27280  wwlksn  29922  wspthsn  29933  rusgrnumwwlklem  30058  clwwlkn  30113  2clwwlk  30434  numclwwlkovh0  30459  numclwwlkovq  30461  shsval  31399  sshjval  31437  faeval  34423  txsconnlem  35453  cvxsconn  35456  iscvm  35472  cvmliftlem5  35502  mpomulnzcnf  36512  rngohomval  38209  rngoisoval  38222  evlselv  42939  prjcrvfval  42983  rmxfval  43255  rmyfval  43256  mendplusg  43533  mendvsca  43538  mnringvald  44563  addrval  44815  subrval  44816  mulvval  44817  sigarval  47202  dmatALTval  48754  naryfval  48982  discsubc  49417  oppfvalg  49479  upfval  49529  setc1onsubc  49955  lmdfval  50002  cmdfval  50003