Theorem ovmpoa 7587

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Vcvv 3477  (class class class)co 7430   ∈ cmpo 7432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435

This theorem is referenced by:  ovmpot  7593  1st2val  8040  2nd2val  8041  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  cantnffval  9700  cantnfsuc  9707  fseqenlem1  10061  xaddval  13261  xmulval  13263  fzoval  13696  expval  14100  ccatfval  14607  splcl  14786  cshfn  14824  bpolylem  16080  ruclem1  16263  sadfval  16485  sadcp1  16488  smufval  16510  smupp1  16513  eucalgval2  16614  pcval  16877  pc0  16887  vdwapval  17006  pwsval  17532  xpsfval  17612  xpsval  17616  rescval  17874  isfunc  17914  isfull  17963  isfth  17967  natfval  18000  catcisolem  18163  xpchom  18235  1stfval  18246  2ndfval  18249  yonedalem3a  18330  yonedainv  18337  plusfval  18672  ismgmhm  18721  ismhm  18810  mulgval  19101  eqgfval  19206  isghm  19245  isga  19321  subgga  19330  cayleylem1  19444  sylow1lem2  19631  isslw  19640  sylow2blem1  19652  sylow3lem1  19659  sylow3lem6  19664  frgpuptinv  19803  frgpup2  19808  isrhm  20494  scafval  20895  islmhm  21043  xrsdsval  21445  ipfval  21684  dsmmval  21771  psrmulfval  21980  mplval  22026  ltbval  22078  mpfrcl  22126  evlsval  22127  evlval  22136  mhpfval  22159  matval  22430  submafval  22600  mdetfval  22607  minmar1fval  22667  txval  23587  xkoval  23610  hmeofval  23781  flffval  24012  qustgplem  24144  dscmet  24600  dscopn  24601  tngval  24667  nmofval  24750  nghmfval  24758  isnmhm  24782  htpyco1  25023  htpycc  25025  phtpycc  25036  reparphti  25042  reparphtiOLD  25043  pcoval  25057  pcohtpylem  25065  pcorevlem  25072  dyadval  25640  itg1addlem3  25746  itg1addlem4  25747  itg1addlem4OLD  25748  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  mdegfval  26115  quotval  26348  elqaalem2  26376  cxpval  26720  cxpcn3  26805  angval  26858  sgmval  27199  lgsval  27359  wwlksn  29866  wspthsn  29877  rusgrnumwwlklem  29999  clwwlkn  30054  2clwwlk  30375  numclwwlkovh0  30400  numclwwlkovq  30402  shsval  31340  sshjval  31378  faeval  34226  txsconnlem  35224  cvxsconn  35227  iscvm  35243  cvmliftlem5  35273  mpomulnzcnf  36281  rngohomval  37950  rngoisoval  37963  evlselv  42573  prjcrvfval  42617  rmxfval  42891  rmyfval  42892  mendplusg  43170  mendvsca  43175  mnringvald  44203  addrval  44461  subrval  44462  mulvval  44463  sigarval  46805  dmatALTval  48245  naryfval  48477