Theorem ovmpoa 7544

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447  (class class class)co 7387   ∈ cmpo 7389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392

This theorem is referenced by:  ovmpot  7550  1st2val  7996  2nd2val  7997  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  cantnffval  9616  cantnfsuc  9623  fseqenlem1  9977  xaddval  13183  xmulval  13185  fzoval  13621  expval  14028  ccatfval  14538  splcl  14717  cshfn  14755  bpolylem  16014  ruclem1  16199  sadfval  16422  sadcp1  16425  smufval  16447  smupp1  16450  eucalgval2  16551  pcval  16815  pc0  16825  vdwapval  16944  pwsval  17449  xpsfval  17529  xpsval  17533  rescval  17789  isfunc  17826  isfull  17874  isfth  17878  natfval  17911  catcisolem  18072  xpchom  18141  1stfval  18152  2ndfval  18155  yonedalem3a  18235  yonedainv  18242  plusfval  18574  ismgmhm  18623  ismhm  18712  mulgval  19003  eqgfval  19108  isghm  19147  isga  19223  subgga  19232  cayleylem1  19342  sylow1lem2  19529  isslw  19538  sylow2blem1  19550  sylow3lem1  19557  sylow3lem6  19562  frgpuptinv  19701  frgpup2  19706  isrhm  20387  scafval  20787  islmhm  20934  xrsdsval  21327  ipfval  21558  dsmmval  21643  psrmulfval  21852  mplval  21898  ltbval  21950  mpfrcl  21992  evlsval  21993  evlval  22002  mhpfval  22025  matval  22298  submafval  22466  mdetfval  22473  minmar1fval  22533  txval  23451  xkoval  23474  hmeofval  23645  flffval  23876  qustgplem  24008  dscmet  24460  dscopn  24461  tngval  24527  nmofval  24602  nghmfval  24610  isnmhm  24634  htpyco1  24877  htpycc  24879  phtpycc  24890  reparphti  24896  reparphtiOLD  24897  pcoval  24911  pcohtpylem  24919  pcorevlem  24926  dyadval  25493  itg1addlem3  25599  itg1addlem4  25600  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  mdegfval  25967  quotval  26200  elqaalem2  26228  cxpval  26573  cxpcn3  26658  angval  26711  sgmval  27052  lgsval  27212  wwlksn  29767  wspthsn  29778  rusgrnumwwlklem  29900  clwwlkn  29955  2clwwlk  30276  numclwwlkovh0  30301  numclwwlkovq  30303  shsval  31241  sshjval  31279  faeval  34236  txsconnlem  35227  cvxsconn  35230  iscvm  35246  cvmliftlem5  35276  mpomulnzcnf  36287  rngohomval  37958  rngoisoval  37971  evlselv  42575  prjcrvfval  42619  rmxfval  42892  rmyfval  42893  mendplusg  43171  mendvsca  43176  mnringvald  44202  addrval  44455  subrval  44456  mulvval  44457  sigarval  46848  dmatALTval  48389  naryfval  48617  discsubc  49053  oppfvalg  49115  upfval  49165  setc1onsubc  49591  lmdfval  49638  cmdfval  49639