Theorem ovmpoa 7547

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450  (class class class)co 7390   ∈ cmpo 7392

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395

This theorem is referenced by:  ovmpot  7553  1st2val  7999  2nd2val  8000  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  cantnffval  9623  cantnfsuc  9630  fseqenlem1  9984  xaddval  13190  xmulval  13192  fzoval  13628  expval  14035  ccatfval  14545  splcl  14724  cshfn  14762  bpolylem  16021  ruclem1  16206  sadfval  16429  sadcp1  16432  smufval  16454  smupp1  16457  eucalgval2  16558  pcval  16822  pc0  16832  vdwapval  16951  pwsval  17456  xpsfval  17536  xpsval  17540  rescval  17796  isfunc  17833  isfull  17881  isfth  17885  natfval  17918  catcisolem  18079  xpchom  18148  1stfval  18159  2ndfval  18162  yonedalem3a  18242  yonedainv  18249  plusfval  18581  ismgmhm  18630  ismhm  18719  mulgval  19010  eqgfval  19115  isghm  19154  isga  19230  subgga  19239  cayleylem1  19349  sylow1lem2  19536  isslw  19545  sylow2blem1  19557  sylow3lem1  19564  sylow3lem6  19569  frgpuptinv  19708  frgpup2  19713  isrhm  20394  scafval  20794  islmhm  20941  xrsdsval  21334  ipfval  21565  dsmmval  21650  psrmulfval  21859  mplval  21905  ltbval  21957  mpfrcl  21999  evlsval  22000  evlval  22009  mhpfval  22032  matval  22305  submafval  22473  mdetfval  22480  minmar1fval  22540  txval  23458  xkoval  23481  hmeofval  23652  flffval  23883  qustgplem  24015  dscmet  24467  dscopn  24468  tngval  24534  nmofval  24609  nghmfval  24617  isnmhm  24641  htpyco1  24884  htpycc  24886  phtpycc  24897  reparphti  24903  reparphtiOLD  24904  pcoval  24918  pcohtpylem  24926  pcorevlem  24933  dyadval  25500  itg1addlem3  25606  itg1addlem4  25607  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  mdegfval  25974  quotval  26207  elqaalem2  26235  cxpval  26580  cxpcn3  26665  angval  26718  sgmval  27059  lgsval  27219  wwlksn  29774  wspthsn  29785  rusgrnumwwlklem  29907  clwwlkn  29962  2clwwlk  30283  numclwwlkovh0  30308  numclwwlkovq  30310  shsval  31248  sshjval  31286  faeval  34243  txsconnlem  35234  cvxsconn  35237  iscvm  35253  cvmliftlem5  35283  mpomulnzcnf  36294  rngohomval  37965  rngoisoval  37978  evlselv  42582  prjcrvfval  42626  rmxfval  42899  rmyfval  42900  mendplusg  43178  mendvsca  43183  mnringvald  44209  addrval  44462  subrval  44463  mulvval  44464  sigarval  46855  dmatALTval  48393  naryfval  48621  discsubc  49057  oppfvalg  49119  upfval  49169  setc1onsubc  49595  lmdfval  49642  cmdfval  49643