Theorem ovmpoa 7515

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430  (class class class)co 7360   ∈ cmpo 7362

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 5231  ax-pr 5370

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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  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 7363  df-oprab 7364  df-mpo 7365

This theorem is referenced by:  ovmpot  7521  1st2val  7963  2nd2val  7964  mptmpoopabbrd  8026  cantnffval  9575  cantnfsuc  9582  fseqenlem1  9937  xaddval  13166  xmulval  13168  fzoval  13605  expval  14016  ccatfval  14526  splcl  14705  cshfn  14743  bpolylem  16004  ruclem1  16189  sadfval  16412  sadcp1  16415  smufval  16437  smupp1  16440  eucalgval2  16541  pcval  16806  pc0  16816  vdwapval  16935  pwsval  17440  xpsfval  17521  xpsval  17525  rescval  17785  isfunc  17822  isfull  17870  isfth  17874  natfval  17907  catcisolem  18068  xpchom  18137  1stfval  18148  2ndfval  18151  yonedalem3a  18231  yonedainv  18238  plusfval  18606  ismgmhm  18655  ismhm  18744  mulgval  19038  eqgfval  19142  isghm  19181  isga  19257  subgga  19266  cayleylem1  19378  sylow1lem2  19565  isslw  19574  sylow2blem1  19586  sylow3lem1  19593  sylow3lem6  19598  frgpuptinv  19737  frgpup2  19742  isrhm  20449  scafval  20867  islmhm  21014  xrsdsval  21400  ipfval  21639  dsmmval  21724  psrmulfval  21932  mplval  21977  ltbval  22031  mpfrcl  22073  evlsval  22074  evlval  22088  mhpfval  22114  matval  22386  submafval  22554  mdetfval  22561  minmar1fval  22621  txval  23539  xkoval  23562  hmeofval  23733  flffval  23964  qustgplem  24096  dscmet  24547  dscopn  24548  tngval  24614  nmofval  24689  nghmfval  24697  isnmhm  24721  htpyco1  24955  htpycc  24957  phtpycc  24968  reparphti  24974  pcoval  24988  pcohtpylem  24996  pcorevlem  25003  dyadval  25569  itg1addlem3  25675  itg1addlem4  25676  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  mdegfval  26037  quotval  26269  elqaalem2  26297  cxpval  26641  cxpcn3  26725  angval  26778  sgmval  27119  lgsval  27278  wwlksn  29920  wspthsn  29931  rusgrnumwwlklem  30056  clwwlkn  30111  2clwwlk  30432  numclwwlkovh0  30457  numclwwlkovq  30459  shsval  31398  sshjval  31436  faeval  34406  txsconnlem  35438  cvxsconn  35441  iscvm  35457  cvmliftlem5  35487  mpomulnzcnf  36497  rngohomval  38299  rngoisoval  38312  evlselv  43034  prjcrvfval  43078  rmxfval  43350  rmyfval  43351  mendplusg  43628  mendvsca  43633  mnringvald  44658  addrval  44910  subrval  44911  mulvval  44912  sigarval  47296  dmatALTval  48888  naryfval  49116  discsubc  49551  oppfvalg  49613  upfval  49663  setc1onsubc  50089  lmdfval  50136  cmdfval  50137