Theorem ovmpoa 7508

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3438  (class class class)co 7353   ∈ cmpo 7355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358

This theorem is referenced by:  ovmpot  7514  1st2val  7959  2nd2val  7960  mptmpoopabbrd  8022  mptmpoopabbrdOLD  8023  cantnffval  9578  cantnfsuc  9585  fseqenlem1  9937  xaddval  13143  xmulval  13145  fzoval  13581  expval  13988  ccatfval  14498  splcl  14676  cshfn  14714  bpolylem  15973  ruclem1  16158  sadfval  16381  sadcp1  16384  smufval  16406  smupp1  16409  eucalgval2  16510  pcval  16774  pc0  16784  vdwapval  16903  pwsval  17408  xpsfval  17488  xpsval  17492  rescval  17752  isfunc  17789  isfull  17837  isfth  17841  natfval  17874  catcisolem  18035  xpchom  18104  1stfval  18115  2ndfval  18118  yonedalem3a  18198  yonedainv  18205  plusfval  18539  ismgmhm  18588  ismhm  18677  mulgval  18968  eqgfval  19073  isghm  19112  isga  19188  subgga  19197  cayleylem1  19309  sylow1lem2  19496  isslw  19505  sylow2blem1  19517  sylow3lem1  19524  sylow3lem6  19529  frgpuptinv  19668  frgpup2  19673  isrhm  20381  scafval  20802  islmhm  20949  xrsdsval  21335  ipfval  21574  dsmmval  21659  psrmulfval  21868  mplval  21914  ltbval  21966  mpfrcl  22008  evlsval  22009  evlval  22018  mhpfval  22041  matval  22314  submafval  22482  mdetfval  22489  minmar1fval  22549  txval  23467  xkoval  23490  hmeofval  23661  flffval  23892  qustgplem  24024  dscmet  24476  dscopn  24477  tngval  24543  nmofval  24618  nghmfval  24626  isnmhm  24650  htpyco1  24893  htpycc  24895  phtpycc  24906  reparphti  24912  reparphtiOLD  24913  pcoval  24927  pcohtpylem  24935  pcorevlem  24942  dyadval  25509  itg1addlem3  25615  itg1addlem4  25616  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1fseqlem6  25637  mdegfval  25983  quotval  26216  elqaalem2  26244  cxpval  26589  cxpcn3  26674  angval  26727  sgmval  27068  lgsval  27228  wwlksn  29800  wspthsn  29811  rusgrnumwwlklem  29933  clwwlkn  29988  2clwwlk  30309  numclwwlkovh0  30334  numclwwlkovq  30336  shsval  31274  sshjval  31312  faeval  34215  txsconnlem  35215  cvxsconn  35218  iscvm  35234  cvmliftlem5  35264  mpomulnzcnf  36275  rngohomval  37946  rngoisoval  37959  evlselv  42563  prjcrvfval  42607  rmxfval  42880  rmyfval  42881  mendplusg  43158  mendvsca  43163  mnringvald  44189  addrval  44442  subrval  44443  mulvval  44444  sigarval  46835  dmatALTval  48389  naryfval  48617  discsubc  49053  oppfvalg  49115  upfval  49165  setc1onsubc  49591  lmdfval  49638  cmdfval  49639