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 5251  ax-pr 5395

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 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  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  13240  xmulval  13242  fzoval  13679  expval  14090  ccatfval  14600  splcl  14779  cshfn  14817  bpolylem  16092  ruclem1  16277  sadfval  16500  sadcp1  16503  smufval  16525  smupp1  16528  eucalgval2  16629  pcval  16894  pc0  16904  vdwapval  17023  pwsval  17529  xpsfval  17610  xpsval  17614  rescval  17874  isfunc  17911  isfull  17959  isfth  17963  natfval  17996  catcisolem  18157  xpchom  18226  1stfval  18237  2ndfval  18240  yonedalem3a  18320  yonedainv  18327  plusfval  18695  ismgmhm  18744  ismhm  18833  mulgval  19128  eqgfval  19235  isghm  19277  isga  19352  subgga  19361  cayleylem1  19473  sylow1lem2  19660  isslw  19669  sylow2blem1  19681  sylow3lem1  19688  sylow3lem6  19693  frgpuptinv  19832  frgpup2  19837  isrhm  20551  scafval  20971  islmhm  21117  xrsdsval  21521  ipfval  21759  dsmmval  21844  psrmulfval  22053  mplval  22098  ltbval  22154  mpfrcl  22196  evlsval  22197  evlval  22211  mhpfval  22261  matval  22529  submafval  22697  mdetfval  22704  minmar1fval  22764  txval  23682  xkoval  23705  hmeofval  23876  flffval  24107  qustgplem  24239  dscmet  24690  dscopn  24691  tngval  24757  nmofval  24832  nghmfval  24840  isnmhm  24864  htpyco1  25098  htpycc  25100  phtpycc  25111  reparphti  25117  pcoval  25131  pcohtpylem  25139  pcorevlem  25146  dyadval  25712  itg1addlem3  25818  itg1addlem4  25819  mbfi1fseqlem3  25837  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  mbfi1fseqlem6  25840  mdegfval  26180  quotval  26414  elqaalem2  26442  cxpval  26787  cxpcn3  26871  angval  26924  sgmval  27264  lgsval  27423  wwlksn  30095  wspthsn  30106  rusgrnumwwlklem  30231  clwwlkn  30286  2clwwlk  30607  numclwwlkovh0  30632  numclwwlkovq  30634  shsval  31573  sshjval  31611  faeval  34553  txsconnlem  35603  cvxsconn  35606  iscvm  35622  cvmliftlem5  35652  mpomulnzcnf  36672  rngohomval  38475  rngoisoval  38488  evlselv  43183  prjcrvfval  43225  rmxfval  43493  rmyfval  43494  mendplusg  43771  mendvsca  43776  mnringvald  44801  addrval  45039  subrval  45040  mulvval  45041  sigarval  47422  dmatALTval  49031  naryfval  49259  discsubc  49693  oppfvalg  49755  upfval  49805  setc1onsubc  50231  lmdfval  50278  cmdfval  50279