Theorem ovmpoa 7562

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3459  (class class class)co 7405   ∈ cmpo 7407

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410

This theorem is referenced by:  ovmpot  7568  1st2val  8016  2nd2val  8017  mptmpoopabbrd  8079  mptmpoopabbrdOLD  8080  cantnffval  9677  cantnfsuc  9684  fseqenlem1  10038  xaddval  13239  xmulval  13241  fzoval  13677  expval  14081  ccatfval  14591  splcl  14770  cshfn  14808  bpolylem  16064  ruclem1  16249  sadfval  16471  sadcp1  16474  smufval  16496  smupp1  16499  eucalgval2  16600  pcval  16864  pc0  16874  vdwapval  16993  pwsval  17500  xpsfval  17580  xpsval  17584  rescval  17840  isfunc  17877  isfull  17925  isfth  17929  natfval  17962  catcisolem  18123  xpchom  18192  1stfval  18203  2ndfval  18206  yonedalem3a  18286  yonedainv  18293  plusfval  18625  ismgmhm  18674  ismhm  18763  mulgval  19054  eqgfval  19159  isghm  19198  isga  19274  subgga  19283  cayleylem1  19393  sylow1lem2  19580  isslw  19589  sylow2blem1  19601  sylow3lem1  19608  sylow3lem6  19613  frgpuptinv  19752  frgpup2  19757  isrhm  20438  scafval  20838  islmhm  20985  xrsdsval  21378  ipfval  21609  dsmmval  21694  psrmulfval  21903  mplval  21949  ltbval  22001  mpfrcl  22043  evlsval  22044  evlval  22053  mhpfval  22076  matval  22349  submafval  22517  mdetfval  22524  minmar1fval  22584  txval  23502  xkoval  23525  hmeofval  23696  flffval  23927  qustgplem  24059  dscmet  24511  dscopn  24512  tngval  24578  nmofval  24653  nghmfval  24661  isnmhm  24685  htpyco1  24928  htpycc  24930  phtpycc  24941  reparphti  24947  reparphtiOLD  24948  pcoval  24962  pcohtpylem  24970  pcorevlem  24977  dyadval  25545  itg1addlem3  25651  itg1addlem4  25652  mbfi1fseqlem3  25670  mbfi1fseqlem4  25671  mbfi1fseqlem5  25672  mbfi1fseqlem6  25673  mdegfval  26019  quotval  26252  elqaalem2  26280  cxpval  26625  cxpcn3  26710  angval  26763  sgmval  27104  lgsval  27264  wwlksn  29819  wspthsn  29830  rusgrnumwwlklem  29952  clwwlkn  30007  2clwwlk  30328  numclwwlkovh0  30353  numclwwlkovq  30355  shsval  31293  sshjval  31331  faeval  34277  txsconnlem  35262  cvxsconn  35265  iscvm  35281  cvmliftlem5  35311  mpomulnzcnf  36317  rngohomval  37988  rngoisoval  38001  evlselv  42610  prjcrvfval  42654  rmxfval  42927  rmyfval  42928  mendplusg  43206  mendvsca  43211  mnringvald  44237  addrval  44490  subrval  44491  mulvval  44492  sigarval  46879  dmatALTval  48376  naryfval  48608  discsubc  49031  oppfvalg  49074  upfval  49111  setc1onsubc  49479  lmdfval  49523  cmdfval  49524