Theorem ovmpoa 7562

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474  (class class class)co 7408   ∈ cmpo 7410

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  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 7411  df-oprab 7412  df-mpo 7413

This theorem is referenced by:  1st2val  8002  2nd2val  8003  mptmpoopabbrd  8066  cantnffval  9657  cantnfsuc  9664  fseqenlem1  10018  xaddval  13201  xmulval  13203  fzoval  13632  expval  14028  ccatfval  14522  splcl  14701  cshfn  14739  bpolylem  15991  ruclem1  16173  sadfval  16392  sadcp1  16395  smufval  16417  smupp1  16420  eucalgval2  16517  pcval  16776  pc0  16786  vdwapval  16905  pwsval  17431  xpsfval  17511  xpsval  17515  rescval  17773  isfunc  17813  isfull  17860  isfth  17864  natfval  17896  catcisolem  18059  xpchom  18131  1stfval  18142  2ndfval  18145  yonedalem3a  18226  yonedainv  18233  plusfval  18567  ismhm  18672  mulgval  18953  eqgfval  19055  isga  19154  subgga  19163  cayleylem1  19279  sylow1lem2  19466  isslw  19475  sylow2blem1  19487  sylow3lem1  19494  sylow3lem6  19499  frgpuptinv  19638  frgpup2  19643  isrhm  20256  scafval  20490  islmhm  20637  xrsdsval  20988  ipfval  21201  dsmmval  21288  psrmulfval  21503  mplval  21547  ltbval  21597  mpfrcl  21647  evlsval  21648  evlval  21657  mhpfval  21681  matval  21910  submafval  22080  mdetfval  22087  minmar1fval  22147  txval  23067  xkoval  23090  hmeofval  23261  flffval  23492  qustgplem  23624  dscmet  24080  dscopn  24081  tngval  24147  nmofval  24230  nghmfval  24238  isnmhm  24262  htpyco1  24493  htpycc  24495  phtpycc  24506  reparphti  24512  pcoval  24526  pcohtpylem  24534  pcorevlem  24541  dyadval  25108  itg1addlem3  25214  itg1addlem4  25215  itg1addlem4OLD  25216  mbfi1fseqlem3  25234  mbfi1fseqlem4  25235  mbfi1fseqlem5  25236  mbfi1fseqlem6  25237  mdegfval  25579  quotval  25804  elqaalem2  25832  cxpval  26171  cxpcn3  26253  angval  26303  sgmval  26643  lgsval  26801  wwlksn  29088  wspthsn  29099  rusgrnumwwlklem  29221  clwwlkn  29276  2clwwlk  29597  numclwwlkovh0  29622  numclwwlkovq  29624  shsval  30560  sshjval  30598  faeval  33239  txsconnlem  34226  cvxsconn  34229  iscvm  34245  cvmliftlem5  34275  gg-reparphti  35167  rngohomval  36827  rngoisoval  36840  evlselv  41161  prjcrvfval  41374  rmxfval  41632  rmyfval  41633  mendplusg  41918  mendvsca  41923  mnringvald  42957  addrval  43215  subrval  43216  mulvval  43217  sigarval  45556  ismgmhm  46543  dmatALTval  47071  naryfval  47304