Theorem ovmpoa 7522

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3429  (class class class)co 7367   ∈ cmpo 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  ovmpot  7528  1st2val  7970  2nd2val  7971  mptmpoopabbrd  8033  cantnffval  9584  cantnfsuc  9591  fseqenlem1  9946  xaddval  13175  xmulval  13177  fzoval  13614  expval  14025  ccatfval  14535  splcl  14714  cshfn  14752  bpolylem  16013  ruclem1  16198  sadfval  16421  sadcp1  16424  smufval  16446  smupp1  16449  eucalgval2  16550  pcval  16815  pc0  16825  vdwapval  16944  pwsval  17449  xpsfval  17530  xpsval  17534  rescval  17794  isfunc  17831  isfull  17879  isfth  17883  natfval  17916  catcisolem  18077  xpchom  18146  1stfval  18157  2ndfval  18160  yonedalem3a  18240  yonedainv  18247  plusfval  18615  ismgmhm  18664  ismhm  18753  mulgval  19047  eqgfval  19151  isghm  19190  isga  19266  subgga  19275  cayleylem1  19387  sylow1lem2  19574  isslw  19583  sylow2blem1  19595  sylow3lem1  19602  sylow3lem6  19607  frgpuptinv  19746  frgpup2  19751  isrhm  20458  scafval  20876  islmhm  21022  xrsdsval  21391  ipfval  21629  dsmmval  21714  psrmulfval  21922  mplval  21967  ltbval  22021  mpfrcl  22063  evlsval  22064  evlval  22078  mhpfval  22104  matval  22376  submafval  22544  mdetfval  22551  minmar1fval  22611  txval  23529  xkoval  23552  hmeofval  23723  flffval  23954  qustgplem  24086  dscmet  24537  dscopn  24538  tngval  24604  nmofval  24679  nghmfval  24687  isnmhm  24711  htpyco1  24945  htpycc  24947  phtpycc  24958  reparphti  24964  pcoval  24978  pcohtpylem  24986  pcorevlem  24993  dyadval  25559  itg1addlem3  25665  itg1addlem4  25666  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  mdegfval  26027  quotval  26258  elqaalem2  26286  cxpval  26628  cxpcn3  26712  angval  26765  sgmval  27105  lgsval  27264  wwlksn  29905  wspthsn  29916  rusgrnumwwlklem  30041  clwwlkn  30096  2clwwlk  30417  numclwwlkovh0  30442  numclwwlkovq  30444  shsval  31383  sshjval  31421  faeval  34390  txsconnlem  35422  cvxsconn  35425  iscvm  35441  cvmliftlem5  35471  mpomulnzcnf  36481  rngohomval  38285  rngoisoval  38298  evlselv  43020  prjcrvfval  43064  rmxfval  43332  rmyfval  43333  mendplusg  43610  mendvsca  43615  mnringvald  44640  addrval  44892  subrval  44893  mulvval  44894  sigarval  47278  dmatALTval  48876  naryfval  49104  discsubc  49539  oppfvalg  49601  upfval  49651  setc1onsubc  50077  lmdfval  50124  cmdfval  50125