Theorem ovmpoa 7555

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  Vcvv 3457  (class class class)co 7400   ∈ cmpo 7402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405

This theorem is referenced by:  ovmpot  7561  1st2val  8002  2nd2val  8003  mptmpoopabbrd  8066  cantnffval  9620  cantnfsuc  9627  fseqenlem1  9996  xaddval  13237  xmulval  13239  fzoval  13676  expval  14087  ccatfval  14598  splcl  14777  cshfn  14815  bpolylem  16090  ruclem1  16275  sadfval  16498  sadcp1  16501  smufval  16523  smupp1  16526  eucalgval2  16627  pcval  16892  pc0  16902  vdwapval  17021  pwsval  17527  xpsfval  17608  xpsval  17612  rescval  17872  isfunc  17909  isfull  17957  isfth  17961  natfval  17994  catcisolem  18155  xpchom  18224  1stfval  18235  2ndfval  18238  yonedalem3a  18318  yonedainv  18325  plusfval  18693  ismgmhm  18742  ismhm  18831  mulgval  19125  eqgfval  19232  isghm  19274  isga  19349  subgga  19358  cayleylem1  19470  sylow1lem2  19657  isslw  19666  sylow2blem1  19678  sylow3lem1  19685  sylow3lem6  19690  frgpuptinv  19829  frgpup2  19834  isrhm  20548  scafval  20968  islmhm  21114  xrsdsval  21518  ipfval  21756  dsmmval  21841  psrmulfval  22050  mplval  22095  ltbval  22151  mpfrcl  22193  evlsval  22194  evlval  22208  mhpfval  22258  matval  22525  submafval  22693  mdetfval  22700  minmar1fval  22760  txval  23678  xkoval  23701  hmeofval  23872  flffval  24103  qustgplem  24235  dscmet  24686  dscopn  24687  tngval  24753  nmofval  24828  nghmfval  24836  isnmhm  24860  htpyco1  25094  htpycc  25096  phtpycc  25107  reparphti  25113  pcoval  25127  pcohtpylem  25135  pcorevlem  25142  dyadval  25708  itg1addlem3  25814  itg1addlem4  25815  mbfi1fseqlem3  25833  mbfi1fseqlem4  25834  mbfi1fseqlem5  25835  mbfi1fseqlem6  25836  mdegfval  26176  quotval  26410  elqaalem2  26438  cxpval  26783  cxpcn3  26867  angval  26920  sgmval  27260  lgsval  27419  wwlksn  30091  wspthsn  30102  rusgrnumwwlklem  30227  clwwlkn  30282  2clwwlk  30603  numclwwlkovh0  30628  numclwwlkovq  30630  shsval  31569  sshjval  31607  faeval  34548  txsconnlem  35598  cvxsconn  35601  iscvm  35617  cvmliftlem5  35647  mpomulnzcnf  36667  rngohomval  38470  rngoisoval  38483  evlselv  43178  prjcrvfval  43220  rmxfval  43488  rmyfval  43489  mendplusg  43766  mendvsca  43771  mnringvald  44796  addrval  45033  subrval  45034  mulvval  45035  sigarval  47423  dmatALTval  49032  naryfval  49260  discsubc  49694  oppfvalg  49756  upfval  49806  setc1onsubc  50232  lmdfval  50279  cmdfval  50280