Theorem ovmpoa 7566

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105  Vcvv 3473  (class class class)co 7412   ∈ cmpo 7414

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417

This theorem is referenced by:  ovmpot  7572  1st2val  8007  2nd2val  8008  mptmpoopabbrd  8071  mptmpoopabbrdOLD  8072  cantnffval  9664  cantnfsuc  9671  fseqenlem1  10025  xaddval  13209  xmulval  13211  fzoval  13640  expval  14036  ccatfval  14530  splcl  14709  cshfn  14747  bpolylem  15999  ruclem1  16181  sadfval  16400  sadcp1  16403  smufval  16425  smupp1  16428  eucalgval2  16525  pcval  16784  pc0  16794  vdwapval  16913  pwsval  17439  xpsfval  17519  xpsval  17523  rescval  17781  isfunc  17821  isfull  17870  isfth  17874  natfval  17907  catcisolem  18070  xpchom  18142  1stfval  18153  2ndfval  18156  yonedalem3a  18237  yonedainv  18244  plusfval  18578  ismgmhm  18627  ismhm  18713  mulgval  18997  eqgfval  19099  isga  19203  subgga  19212  cayleylem1  19328  sylow1lem2  19515  isslw  19524  sylow2blem1  19536  sylow3lem1  19543  sylow3lem6  19548  frgpuptinv  19687  frgpup2  19692  isrhm  20376  scafval  20723  islmhm  20871  xrsdsval  21278  ipfval  21512  dsmmval  21599  psrmulfval  21815  mplval  21859  ltbval  21909  mpfrcl  21959  evlsval  21960  evlval  21969  mhpfval  21991  matval  22231  submafval  22401  mdetfval  22408  minmar1fval  22468  txval  23388  xkoval  23411  hmeofval  23582  flffval  23813  qustgplem  23945  dscmet  24401  dscopn  24402  tngval  24468  nmofval  24551  nghmfval  24559  isnmhm  24583  htpyco1  24824  htpycc  24826  phtpycc  24837  reparphti  24843  reparphtiOLD  24844  pcoval  24858  pcohtpylem  24866  pcorevlem  24873  dyadval  25441  itg1addlem3  25547  itg1addlem4  25548  itg1addlem4OLD  25549  mbfi1fseqlem3  25567  mbfi1fseqlem4  25568  mbfi1fseqlem5  25569  mbfi1fseqlem6  25570  mdegfval  25918  quotval  26144  elqaalem2  26172  cxpval  26512  cxpcn3  26597  angval  26647  sgmval  26987  lgsval  27147  wwlksn  29524  wspthsn  29535  rusgrnumwwlklem  29657  clwwlkn  29712  2clwwlk  30033  numclwwlkovh0  30058  numclwwlkovq  30060  shsval  30998  sshjval  31036  faeval  33708  txsconnlem  34695  cvxsconn  34698  iscvm  34714  cvmliftlem5  34744  mpomulnzcnf  35629  rngohomval  37296  rngoisoval  37309  evlselv  41622  prjcrvfval  41836  rmxfval  42105  rmyfval  42106  mendplusg  42391  mendvsca  42396  mnringvald  43430  addrval  43688  subrval  43689  mulvval  43690  sigarval  46025  dmatALTval  47243  naryfval  47476