Theorem ovmpoa 7588

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480  (class class class)co 7431   ∈ cmpo 7433

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436

This theorem is referenced by:  ovmpot  7594  1st2val  8042  2nd2val  8043  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  cantnffval  9703  cantnfsuc  9710  fseqenlem1  10064  xaddval  13265  xmulval  13267  fzoval  13700  expval  14104  ccatfval  14611  splcl  14790  cshfn  14828  bpolylem  16084  ruclem1  16267  sadfval  16489  sadcp1  16492  smufval  16514  smupp1  16517  eucalgval2  16618  pcval  16882  pc0  16892  vdwapval  17011  pwsval  17531  xpsfval  17611  xpsval  17615  rescval  17871  isfunc  17909  isfull  17957  isfth  17961  natfval  17994  catcisolem  18155  xpchom  18225  1stfval  18236  2ndfval  18239  yonedalem3a  18319  yonedainv  18326  plusfval  18660  ismgmhm  18709  ismhm  18798  mulgval  19089  eqgfval  19194  isghm  19233  isga  19309  subgga  19318  cayleylem1  19430  sylow1lem2  19617  isslw  19626  sylow2blem1  19638  sylow3lem1  19645  sylow3lem6  19650  frgpuptinv  19789  frgpup2  19794  isrhm  20478  scafval  20879  islmhm  21026  xrsdsval  21428  ipfval  21667  dsmmval  21754  psrmulfval  21963  mplval  22009  ltbval  22061  mpfrcl  22109  evlsval  22110  evlval  22119  mhpfval  22142  matval  22415  submafval  22585  mdetfval  22592  minmar1fval  22652  txval  23572  xkoval  23595  hmeofval  23766  flffval  23997  qustgplem  24129  dscmet  24585  dscopn  24586  tngval  24652  nmofval  24735  nghmfval  24743  isnmhm  24767  htpyco1  25010  htpycc  25012  phtpycc  25023  reparphti  25029  reparphtiOLD  25030  pcoval  25044  pcohtpylem  25052  pcorevlem  25059  dyadval  25627  itg1addlem3  25733  itg1addlem4  25734  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  mdegfval  26101  quotval  26334  elqaalem2  26362  cxpval  26706  cxpcn3  26791  angval  26844  sgmval  27185  lgsval  27345  wwlksn  29857  wspthsn  29868  rusgrnumwwlklem  29990  clwwlkn  30045  2clwwlk  30366  numclwwlkovh0  30391  numclwwlkovq  30393  shsval  31331  sshjval  31369  faeval  34247  txsconnlem  35245  cvxsconn  35248  iscvm  35264  cvmliftlem5  35294  mpomulnzcnf  36300  rngohomval  37971  rngoisoval  37984  evlselv  42597  prjcrvfval  42641  rmxfval  42915  rmyfval  42916  mendplusg  43194  mendvsca  43199  mnringvald  44227  addrval  44485  subrval  44486  mulvval  44487  sigarval  46865  dmatALTval  48317  naryfval  48549  upfval  48933