Theorem ovmpoa 7565

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  Vcvv 3472  (class class class)co 7411   ∈ cmpo 7413

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  1st2val  8005  2nd2val  8006  mptmpoopabbrd  8069  cantnffval  9660  cantnfsuc  9667  fseqenlem1  10021  ovmul  11207  xaddval  13206  xmulval  13208  fzoval  13637  expval  14033  ccatfval  14527  splcl  14706  cshfn  14744  bpolylem  15996  ruclem1  16178  sadfval  16397  sadcp1  16400  smufval  16422  smupp1  16425  eucalgval2  16522  pcval  16781  pc0  16791  vdwapval  16910  pwsval  17436  xpsfval  17516  xpsval  17520  rescval  17778  isfunc  17818  isfull  17865  isfth  17869  natfval  17901  catcisolem  18064  xpchom  18136  1stfval  18147  2ndfval  18150  yonedalem3a  18231  yonedainv  18238  plusfval  18572  ismgmhm  18621  ismhm  18707  mulgval  18990  eqgfval  19092  isga  19196  subgga  19205  cayleylem1  19321  sylow1lem2  19508  isslw  19517  sylow2blem1  19529  sylow3lem1  19536  sylow3lem6  19541  frgpuptinv  19680  frgpup2  19685  isrhm  20369  scafval  20635  islmhm  20782  xrsdsval  21189  ipfval  21421  dsmmval  21508  psrmulfval  21723  mplval  21767  ltbval  21817  mpfrcl  21867  evlsval  21868  evlval  21877  mhpfval  21901  matval  22131  submafval  22301  mdetfval  22308  minmar1fval  22368  txval  23288  xkoval  23311  hmeofval  23482  flffval  23713  qustgplem  23845  dscmet  24301  dscopn  24302  tngval  24368  nmofval  24451  nghmfval  24459  isnmhm  24483  htpyco1  24724  htpycc  24726  phtpycc  24737  reparphti  24743  reparphtiOLD  24744  pcoval  24758  pcohtpylem  24766  pcorevlem  24773  dyadval  25341  itg1addlem3  25447  itg1addlem4  25448  itg1addlem4OLD  25449  mbfi1fseqlem3  25467  mbfi1fseqlem4  25468  mbfi1fseqlem5  25469  mbfi1fseqlem6  25470  mdegfval  25815  quotval  26041  elqaalem2  26069  cxpval  26408  cxpcn3  26492  angval  26542  sgmval  26882  lgsval  27040  wwlksn  29358  wspthsn  29369  rusgrnumwwlklem  29491  clwwlkn  29546  2clwwlk  29867  numclwwlkovh0  29892  numclwwlkovq  29894  shsval  30832  sshjval  30870  faeval  33542  txsconnlem  34529  cvxsconn  34532  iscvm  34548  cvmliftlem5  34578  rngohomval  37135  rngoisoval  37148  evlselv  41461  prjcrvfval  41675  rmxfval  41944  rmyfval  41945  mendplusg  42230  mendvsca  42235  mnringvald  43269  addrval  43527  subrval  43528  mulvval  43529  sigarval  45864  dmatALTval  47168  naryfval  47401