Theorem ovmpoa 7428

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432  (class class class)co 7275   ∈ cmpo 7277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280

This theorem is referenced by:  1st2val  7859  2nd2val  7860  mptmpoopabbrd  7921  cantnffval  9421  cantnfsuc  9428  fseqenlem1  9780  xaddval  12957  xmulval  12959  fzoval  13388  expval  13784  ccatfval  14276  splcl  14465  cshfn  14503  bpolylem  15758  ruclem1  15940  sadfval  16159  sadcp1  16162  smufval  16184  smupp1  16187  eucalgval2  16286  pcval  16545  pc0  16555  vdwapval  16674  pwsval  17197  xpsfval  17277  xpsval  17281  rescval  17539  isfunc  17579  isfull  17626  isfth  17630  natfval  17662  catcisolem  17825  xpchom  17897  1stfval  17908  2ndfval  17911  yonedalem3a  17992  yonedainv  17999  plusfval  18333  ismhm  18432  mulgval  18704  eqgfval  18804  isga  18897  subgga  18906  cayleylem1  19020  sylow1lem2  19204  isslw  19213  sylow2blem1  19225  sylow3lem1  19232  sylow3lem6  19237  frgpuptinv  19377  frgpup2  19382  isrhm  19965  scafval  20142  islmhm  20289  xrsdsval  20642  ipfval  20854  dsmmval  20941  psrmulfval  21154  mplval  21197  ltbval  21244  mpfrcl  21295  evlsval  21296  evlval  21305  mhpfval  21329  matval  21558  submafval  21728  mdetfval  21735  minmar1fval  21795  txval  22715  xkoval  22738  hmeofval  22909  flffval  23140  qustgplem  23272  dscmet  23728  dscopn  23729  tngval  23795  nmofval  23878  nghmfval  23886  isnmhm  23910  htpyco1  24141  htpycc  24143  phtpycc  24154  reparphti  24160  pcoval  24174  pcohtpylem  24182  pcorevlem  24189  dyadval  24756  itg1addlem3  24862  itg1addlem4  24863  itg1addlem4OLD  24864  mbfi1fseqlem3  24882  mbfi1fseqlem4  24883  mbfi1fseqlem5  24884  mbfi1fseqlem6  24885  mdegfval  25227  quotval  25452  elqaalem2  25480  cxpval  25819  cxpcn3  25901  angval  25951  sgmval  26291  lgsval  26449  wwlksn  28202  wspthsn  28213  rusgrnumwwlklem  28335  clwwlkn  28390  2clwwlk  28711  numclwwlkovh0  28736  numclwwlkovq  28738  shsval  29674  sshjval  29712  faeval  32214  txsconnlem  33202  cvxsconn  33205  iscvm  33221  cvmliftlem5  33251  rngohomval  36122  rngoisoval  36135  prjcrvfval  40468  rmxfval  40726  rmyfval  40727  mendplusg  41011  mendvsca  41016  mnringvald  41826  addrval  42084  subrval  42085  mulvval  42086  sigarval  44366  ismgmhm  45337  dmatALTval  45741  naryfval  45974