Theorem ovmpo 7520

Description: Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Hypotheses

Ref	Expression
ovmpog.1	⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)
ovmpog.2	⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)
ovmpog.3	⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
ovmpo.4	⊢ 𝑆 ∈ V

Assertion

Ref	Expression
ovmpo	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦

Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem ovmpo

Step	Hyp	Ref	Expression
1		ovmpo.4	. 2 ⊢ 𝑆 ∈ V
2		ovmpog.1	. . 3 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)
3		ovmpog.2	. . 3 ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)
4		ovmpog.3	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
5	2, 3, 4	ovmpog 7519	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
6	1, 5	mp3an3 1459	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ∈ wcel 2121  Vcvv 3433  (class class class)co 7360   ∈ cmpo 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6445  df-fun 6491  df-fv 6497  df-ov 7363  df-oprab 7364  df-mpo 7365

This theorem is referenced by:  fvproj  8078  seqomlem1  8383  seqomlem4  8386  oav  8440  omv  8441  oev  8443  iunfictbso  10031  fin23lem12  10248  axdc4lem  10372  axcclem  10374  addpipq2  10854  mulpipq2  10857  subval  11379  divval  11806  cnref1o  12930  ixxval  13301  fzval  13458  modval  13825  om2uzrdg  13913  uzrdgsuci  13917  axdc4uzlem  13940  seqval  13969  seqp1  13973  bcval  14261  cnrecnv  15122  risefacval  15968  fallfacval  15969  gcdval  16460  lcmval  16556  imasvscafn  17496  imasvscaval  17497  grpsubval  18956  isghmOLD  19186  lactghmga  19375  efgmval  19682  efgtval  19693  frgpup3lem  19747  dvrval  20378  frlmval  21727  psrvsca  21928  mat1comp  22427  mamulid  22428  mamurid  22429  madufval  22624  xkococnlem  23646  xkococn  23647  cnextval  24048  dscmet  24559  cncfval  24877  htpycom  24965  htpyid  24966  phtpycom  24977  phtpyid  24978  ehl1eudisval  25410  logbval  26752  addsval  27976  subsval  28074  mulsval  28123  divsval  28203  seqsval  28302  om2noseqrdg  28318  noseqrdgsuc  28322  seqsp1  28325  expsval  28439  isismt  28624  clwwlknon  30182  clwwlk0on0  30184  grpodivval  30628  ipval  30796  lnoval  30845  nmoofval  30855  bloval  30874  0ofval  30880  ajfval  30902  hvsubval  31109  hosmval  31828  hommval  31829  hodmval  31830  hfsmval  31831  hfmmval  31832  kbfval  32045  opsqrlem3  32235  dpval  32972  xdivval  33001  smatrcl  33992  smatlem  33993  mdetpmtr12  34021  pstmfval  34092  sxval  34386  ismbfm  34447  dya2iocival  34469  sitgval  34528  sitmval  34545  oddpwdcv  34551  ballotlemgval  34720  vtsval  34833  cvmlift2lem4  35549  icoreval  37730  metf1o  38137  heiborlem3  38195  heiborlem6  38198  heiborlem8  38200  heibor  38203  ldualvs  39644  tendopl  41283  cdlemkuu  41402  dvavsca  41524  dvhvaddval  41597  dvhvscaval  41606  hlhilipval  42456  resubval  42859  redivvald  42934  prjspnval  43081  rrx2xpref1o  49223  fuco22natlem  49849  functhinclem1  49948