Theorem ovmpoa 7161

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081  Vcvv 3437  (class class class)co 7016   ∈ cmpo 7018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-iota 6189  df-fun 6227  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021

This theorem is referenced by:  1st2val  7573  2nd2val  7574  cantnffval  8972  cantnfsuc  8979  fseqenlem1  9296  xaddval  12466  xmulval  12468  fzoval  12889  expval  13281  ccatfval  13771  splcl  13950  cshfn  13988  bpolylem  15235  ruclem1  15417  sadfval  15634  sadcp1  15637  smufval  15659  smupp1  15662  eucalgval2  15754  pcval  16010  pc0  16020  vdwapval  16138  pwsval  16588  xpsfval  16668  xpsval  16672  rescval  16926  isfunc  16963  isfull  17009  isfth  17013  natfval  17045  catcisolem  17195  xpchom  17259  1stfval  17270  2ndfval  17273  yonedalem3a  17353  yonedainv  17360  plusfval  17687  ismhm  17776  mulgval  17985  eqgfval  18081  isga  18162  subgga  18171  cayleylem1  18271  sylow1lem2  18454  isslw  18463  sylow2blem1  18475  sylow3lem1  18482  sylow3lem6  18487  frgpuptinv  18624  frgpup2  18629  isrhm  19163  scafval  19343  islmhm  19489  psrmulfval  19853  mplval  19896  ltbval  19939  mpfrcl  19985  evlsval  19986  evlval  19991  xrsdsval  20271  ipfval  20475  dsmmval  20560  matval  20704  submafval  20872  mdetfval  20879  minmar1fval  20939  txval  21856  xkoval  21879  hmeofval  22050  flffval  22281  qustgplem  22412  dscmet  22865  dscopn  22866  tngval  22931  nmofval  23006  nghmfval  23014  isnmhm  23038  htpyco1  23265  htpycc  23267  phtpycc  23278  reparphti  23284  pcoval  23298  pcohtpylem  23306  pcorevlem  23313  dyadval  23876  itg1addlem3  23982  itg1addlem4  23983  mbfi1fseqlem3  24001  mbfi1fseqlem4  24002  mbfi1fseqlem5  24003  mbfi1fseqlem6  24004  mdegfval  24339  quotval  24564  elqaalem2  24592  cxpval  24928  cxpcn3  25010  angval  25060  sgmval  25401  lgsval  25559  wwlksn  27302  wspthsn  27313  rusgrnumwwlklem  27436  clwwlkn  27491  2clwwlk  27818  numclwwlkovh0  27843  numclwwlkovq  27845  shsval  28780  sshjval  28818  faeval  31122  txsconnlem  32095  cvxsconn  32098  iscvm  32114  cvmliftlem5  32144  rngohomval  34774  rngoisoval  34787  rmxfval  38986  rmyfval  38987  mendplusg  39271  mendvsca  39276  addrval  40337  subrval  40338  mulvval  40339  sigarval  42649  ismgmhm  43532  dmatALTval  43935