Theorem ovmpoa 7518

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3432  (class class class)co 7363   ∈ cmpo 7365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368

This theorem is referenced by:  ovmpot  7524  1st2val  7966  2nd2val  7967  mptmpoopabbrd  8029  cantnffval  9582  cantnfsuc  9589  fseqenlem1  9944  xaddval  13173  xmulval  13175  fzoval  13612  expval  14023  ccatfval  14533  splcl  14712  cshfn  14750  bpolylem  16011  ruclem1  16196  sadfval  16419  sadcp1  16422  smufval  16444  smupp1  16447  eucalgval2  16548  pcval  16813  pc0  16823  vdwapval  16942  pwsval  17447  xpsfval  17528  xpsval  17532  rescval  17792  isfunc  17829  isfull  17877  isfth  17881  natfval  17914  catcisolem  18075  xpchom  18144  1stfval  18155  2ndfval  18158  yonedalem3a  18238  yonedainv  18245  plusfval  18613  ismgmhm  18662  ismhm  18751  mulgval  19045  eqgfval  19149  isghm  19188  isga  19264  subgga  19273  cayleylem1  19385  sylow1lem2  19572  isslw  19581  sylow2blem1  19593  sylow3lem1  19600  sylow3lem6  19605  frgpuptinv  19744  frgpup2  19749  isrhm  20456  scafval  20878  islmhm  21024  xrsdsval  21393  ipfval  21631  dsmmval  21716  psrmulfval  21925  mplval  21970  ltbval  22026  mpfrcl  22068  evlsval  22069  evlval  22083  mhpfval  22133  matval  22401  submafval  22569  mdetfval  22576  minmar1fval  22636  txval  23554  xkoval  23577  hmeofval  23748  flffval  23979  qustgplem  24111  dscmet  24562  dscopn  24563  tngval  24629  nmofval  24704  nghmfval  24712  isnmhm  24736  htpyco1  24970  htpycc  24972  phtpycc  24983  reparphti  24989  pcoval  25003  pcohtpylem  25011  pcorevlem  25018  dyadval  25584  itg1addlem3  25690  itg1addlem4  25691  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1fseqlem6  25712  mdegfval  26052  quotval  26283  elqaalem2  26311  cxpval  26653  cxpcn3  26737  angval  26790  sgmval  27130  lgsval  27289  wwlksn  29930  wspthsn  29941  rusgrnumwwlklem  30066  clwwlkn  30121  2clwwlk  30442  numclwwlkovh0  30467  numclwwlkovq  30469  shsval  31408  sshjval  31446  faeval  34437  txsconnlem  35475  cvxsconn  35478  iscvm  35494  cvmliftlem5  35524  mpomulnzcnf  36534  rngohomval  38338  rngoisoval  38351  evlselv  43046  prjcrvfval  43088  rmxfval  43356  rmyfval  43357  mendplusg  43634  mendvsca  43639  mnringvald  44664  addrval  44916  subrval  44917  mulvval  44918  sigarval  47300  dmatALTval  48898  naryfval  49126  discsubc  49561  oppfvalg  49623  upfval  49673  setc1onsubc  50099  lmdfval  50146  cmdfval  50147