Theorem ovmpoa 7507

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3437  (class class class)co 7352   ∈ cmpo 7354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357

This theorem is referenced by:  ovmpot  7513  1st2val  7955  2nd2val  7956  mptmpoopabbrd  8018  mptmpoopabbrdOLD  8019  cantnffval  9560  cantnfsuc  9567  fseqenlem1  9922  xaddval  13124  xmulval  13126  fzoval  13562  expval  13972  ccatfval  14482  splcl  14661  cshfn  14699  bpolylem  15957  ruclem1  16142  sadfval  16365  sadcp1  16368  smufval  16390  smupp1  16393  eucalgval2  16494  pcval  16758  pc0  16768  vdwapval  16887  pwsval  17392  xpsfval  17472  xpsval  17476  rescval  17736  isfunc  17773  isfull  17821  isfth  17825  natfval  17858  catcisolem  18019  xpchom  18088  1stfval  18099  2ndfval  18102  yonedalem3a  18182  yonedainv  18189  plusfval  18557  ismgmhm  18606  ismhm  18695  mulgval  18986  eqgfval  19090  isghm  19129  isga  19205  subgga  19214  cayleylem1  19326  sylow1lem2  19513  isslw  19522  sylow2blem1  19534  sylow3lem1  19541  sylow3lem6  19546  frgpuptinv  19685  frgpup2  19690  isrhm  20398  scafval  20816  islmhm  20963  xrsdsval  21349  ipfval  21588  dsmmval  21673  psrmulfval  21882  mplval  21927  ltbval  21979  mpfrcl  22021  evlsval  22022  evlval  22031  mhpfval  22054  matval  22327  submafval  22495  mdetfval  22502  minmar1fval  22562  txval  23480  xkoval  23503  hmeofval  23674  flffval  23905  qustgplem  24037  dscmet  24488  dscopn  24489  tngval  24555  nmofval  24630  nghmfval  24638  isnmhm  24662  htpyco1  24905  htpycc  24907  phtpycc  24918  reparphti  24924  reparphtiOLD  24925  pcoval  24939  pcohtpylem  24947  pcorevlem  24954  dyadval  25521  itg1addlem3  25627  itg1addlem4  25628  mbfi1fseqlem3  25646  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649  mdegfval  25995  quotval  26228  elqaalem2  26256  cxpval  26601  cxpcn3  26686  angval  26739  sgmval  27080  lgsval  27240  wwlksn  29817  wspthsn  29828  rusgrnumwwlklem  29953  clwwlkn  30008  2clwwlk  30329  numclwwlkovh0  30354  numclwwlkovq  30356  shsval  31294  sshjval  31332  faeval  34280  txsconnlem  35305  cvxsconn  35308  iscvm  35324  cvmliftlem5  35354  mpomulnzcnf  36364  rngohomval  38025  rngoisoval  38038  evlselv  42706  prjcrvfval  42750  rmxfval  43022  rmyfval  43023  mendplusg  43300  mendvsca  43305  mnringvald  44331  addrval  44583  subrval  44584  mulvval  44585  sigarval  46973  dmatALTval  48526  naryfval  48754  discsubc  49190  oppfvalg  49252  upfval  49302  setc1onsubc  49728  lmdfval  49775  cmdfval  49776