Theorem ovmpoa 7572

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3453  (class class class)co 7417   ∈ cmpo 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422

This theorem is used by:  ovmpot  7578  1st2val  8018  2nd2val  8019  mptmpoopabbrd  8084  cantnffval  9646  cantnfsuc  9653  fseqenlem1  10031  xaddval  13279  xmulval  13281  fzoval  13719  expval  14131  ccatfval  14642  splcl  14825  cshfn  14865  bpolylem  16140  ruclem1  16325  sadfval  16548  sadcp1  16551  smufval  16573  smupp1  16576  eucalgval2  16677  pcval  16942  pc0  16952  vdwapval  17071  pwsval  17577  xpsfval  17658  xpsval  17662  rescval  17922  isfunc  17959  isfull  18007  isfth  18011  natfval  18044  catcisolem  18205  xpchom  18274  1stfval  18285  2ndfval  18288  yonedalem3a  18368  yonedainv  18375  plusfval  18743  ismgmhm  18804  ismhm  18899  mulgval  19200  eqgfval  19307  isghm  19349  isga  19424  subgga  19433  cayleylem1  19545  sylow1lem2  19732  isslw  19741  sylow2blem1  19753  sylow3lem1  19760  sylow3lem6  19765  frgpuptinv  19904  frgpup2  19909  rhmval0  20622  isrhm  20626  scafval  21071  islmhm  21217  xrsdsval  21630  ipfval  21868  dsmmval  21953  psrmulfval  22164  mplval  22209  ltbval  22265  mpfrcl  22307  evlsval  22308  evlval  22322  mhpfval  22372  matval  22639  submafval  22807  mdetfval  22814  minmar1fval  22874  txval  23796  xkoval  23819  hmeofval  23990  flffval  24221  qustgplem  24353  dscmet  24804  dscopn  24805  tngval  24871  nmofval  24946  nghmfval  24954  isnmhm  24978  htpyco1  25212  htpycc  25214  phtpycc  25225  reparphti  25231  pcoval  25245  pcohtpylem  25253  pcorevlem  25260  dyadval  25826  itg1addlem3  25932  itg1addlem4  25933  mbfi1fseqlem3  25951  mbfi1fseqlem4  25952  mbfi1fseqlem5  25953  mbfi1fseqlem6  25954  mdegfval  26294  quotval  26529  elqaalem2  26559  cxpval  26909  cxpcn3  26993  angval  27046  sgmval  27386  lgsval  27545  wwlksn  30313  wspthsn  30324  rusgrnumwwlklem  30449  clwwlkn  30504  2clwwlk  30835  numclwwlkovh0  30860  numclwwlkovq  30862  shsval  31801  sshjval  31839  faeval  34765  txsconnlem  35827  cvxsconn  35830  iscvm  35846  cvmliftlem5  35876  mpomulnzcnf  36927  rngohomval  38722  rngoisoval  38735  evlselv  43443  prjcrvfval  43485  rmxfval  43753  rmyfval  43754  mendplusg  44031  mendvsca  44036  mnringvald  45059  addrval  45296  subrval  45297  mulvval  45298  sigarval  47686  dmatALTval  49338  naryfval  49566  discsubc  49998  oppfvalg  50060  upfval  50110  setc1onsubc  50536  lmdfval  50583  cmdfval  50584