Theorem ovmpoa 7501

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436  (class class class)co 7346   ∈ cmpo 7348

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351

This theorem is referenced by:  ovmpot  7507  1st2val  7949  2nd2val  7950  mptmpoopabbrd  8012  mptmpoopabbrdOLD  8013  cantnffval  9553  cantnfsuc  9560  fseqenlem1  9915  xaddval  13122  xmulval  13124  fzoval  13560  expval  13970  ccatfval  14480  splcl  14659  cshfn  14697  bpolylem  15955  ruclem1  16140  sadfval  16363  sadcp1  16366  smufval  16388  smupp1  16391  eucalgval2  16492  pcval  16756  pc0  16766  vdwapval  16885  pwsval  17390  xpsfval  17470  xpsval  17474  rescval  17734  isfunc  17771  isfull  17819  isfth  17823  natfval  17856  catcisolem  18017  xpchom  18086  1stfval  18097  2ndfval  18100  yonedalem3a  18180  yonedainv  18187  plusfval  18555  ismgmhm  18604  ismhm  18693  mulgval  18984  eqgfval  19089  isghm  19128  isga  19204  subgga  19213  cayleylem1  19325  sylow1lem2  19512  isslw  19521  sylow2blem1  19533  sylow3lem1  19540  sylow3lem6  19545  frgpuptinv  19684  frgpup2  19689  isrhm  20397  scafval  20815  islmhm  20962  xrsdsval  21348  ipfval  21587  dsmmval  21672  psrmulfval  21881  mplval  21927  ltbval  21979  mpfrcl  22021  evlsval  22022  evlval  22031  mhpfval  22054  matval  22327  submafval  22495  mdetfval  22502  minmar1fval  22562  txval  23480  xkoval  23503  hmeofval  23674  flffval  23905  qustgplem  24037  dscmet  24488  dscopn  24489  tngval  24555  nmofval  24630  nghmfval  24638  isnmhm  24662  htpyco1  24905  htpycc  24907  phtpycc  24918  reparphti  24924  reparphtiOLD  24925  pcoval  24939  pcohtpylem  24947  pcorevlem  24954  dyadval  25521  itg1addlem3  25627  itg1addlem4  25628  mbfi1fseqlem3  25646  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649  mdegfval  25995  quotval  26228  elqaalem2  26256  cxpval  26601  cxpcn3  26686  angval  26739  sgmval  27080  lgsval  27240  wwlksn  29816  wspthsn  29827  rusgrnumwwlklem  29949  clwwlkn  30004  2clwwlk  30325  numclwwlkovh0  30350  numclwwlkovq  30352  shsval  31290  sshjval  31328  faeval  34257  txsconnlem  35282  cvxsconn  35285  iscvm  35301  cvmliftlem5  35331  mpomulnzcnf  36339  rngohomval  38010  rngoisoval  38023  evlselv  42626  prjcrvfval  42670  rmxfval  42943  rmyfval  42944  mendplusg  43221  mendvsca  43226  mnringvald  44252  addrval  44504  subrval  44505  mulvval  44506  sigarval  46894  dmatALTval  48438  naryfval  48666  discsubc  49102  oppfvalg  49164  upfval  49214  setc1onsubc  49640  lmdfval  49687  cmdfval  49688