Theorem ovmpoa 7578

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3458  (class class class)co 7423   ∈ cmpo 7425

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428

This theorem is used by:  ovmpot  7584  1st2val  8023  2nd2val  8024  mptmpoopabbrd  8087  cantnffval  9642  cantnfsuc  9649  fseqenlem1  10027  xaddval  13267  xmulval  13269  fzoval  13707  expval  14119  ccatfval  14630  splcl  14813  cshfn  14853  bpolylem  16127  ruclem1  16312  sadfval  16535  sadcp1  16538  smufval  16560  smupp1  16563  eucalgval2  16664  pcval  16929  pc0  16939  vdwapval  17058  pwsval  17564  xpsfval  17645  xpsval  17649  rescval  17909  isfunc  17946  isfull  17994  isfth  17998  natfval  18031  catcisolem  18192  xpchom  18261  1stfval  18272  2ndfval  18275  yonedalem3a  18355  yonedainv  18362  plusfval  18730  ismgmhm  18783  ismhm  18874  mulgval  19168  eqgfval  19275  isghm  19317  isga  19392  subgga  19401  cayleylem1  19513  sylow1lem2  19700  isslw  19709  sylow2blem1  19721  sylow3lem1  19728  sylow3lem6  19733  frgpuptinv  19872  frgpup2  19877  rhmval0  20590  isrhm  20594  scafval  21039  islmhm  21185  xrsdsval  21598  ipfval  21836  dsmmval  21921  psrmulfval  22130  mplval  22175  ltbval  22231  mpfrcl  22273  evlsval  22274  evlval  22288  mhpfval  22338  matval  22605  submafval  22773  mdetfval  22780  minmar1fval  22840  txval  23758  xkoval  23781  hmeofval  23952  flffval  24183  qustgplem  24315  dscmet  24766  dscopn  24767  tngval  24833  nmofval  24908  nghmfval  24916  isnmhm  24940  htpyco1  25174  htpycc  25176  phtpycc  25187  reparphti  25193  pcoval  25207  pcohtpylem  25215  pcorevlem  25222  dyadval  25788  itg1addlem3  25894  itg1addlem4  25895  mbfi1fseqlem3  25913  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  mbfi1fseqlem6  25916  mdegfval  26256  quotval  26490  elqaalem2  26518  cxpval  26866  cxpcn3  26950  angval  27003  sgmval  27343  lgsval  27502  wwlksn  30223  wspthsn  30234  rusgrnumwwlklem  30359  clwwlkn  30414  2clwwlk  30735  numclwwlkovh0  30760  numclwwlkovq  30762  shsval  31701  sshjval  31739  faeval  34668  txsconnlem  35753  cvxsconn  35756  iscvm  35772  cvmliftlem5  35802  mpomulnzcnf  36852  rngohomval  38656  rngoisoval  38669  evlselv  43362  prjcrvfval  43404  rmxfval  43672  rmyfval  43673  mendplusg  43950  mendvsca  43955  mnringvald  44978  addrval  45215  subrval  45216  mulvval  45217  sigarval  47605  dmatALTval  49221  naryfval  49449  discsubc  49883  oppfvalg  49945  upfval  49995  setc1onsubc  50421  lmdfval  50468  cmdfval  50469