Theorem ovmpo 7592

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Vcvv 3477  (class class class)co 7430   ∈ cmpo 7432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435

This theorem is referenced by:  fvproj  8157  seqomlem1  8488  seqomlem4  8491  oav  8547  omv  8548  oev  8550  iunfictbso  10151  fin23lem12  10368  axdc4lem  10492  axcclem  10494  addpipq2  10973  mulpipq2  10976  subval  11496  divval  11921  cnref1o  13024  ixxval  13391  fzval  13545  modval  13907  om2uzrdg  13993  uzrdgsuci  13997  axdc4uzlem  14020  seqval  14049  seqp1  14053  bcval  14339  cnrecnv  15200  risefacval  16040  fallfacval  16041  gcdval  16529  lcmval  16625  imasvscafn  17583  imasvscaval  17584  grpsubval  19015  isghmOLD  19246  lactghmga  19437  efgmval  19744  efgtval  19755  frgpup3lem  19809  dvrval  20419  frlmval  21785  psrvsca  21986  mat1comp  22461  mamulid  22462  mamurid  22463  madufval  22658  xkococnlem  23682  xkococn  23683  cnextval  24084  dscmet  24600  cncfval  24927  htpycom  25021  htpyid  25022  phtpycom  25033  phtpyid  25034  ehl1eudisval  25468  logbval  26823  addsval  28009  subsval  28104  mulsval  28149  divsval  28229  seqsval  28308  om2noseqrdg  28324  noseqrdgsuc  28328  seqsp1  28331  expsval  28422  isismt  28556  clwwlknon  30118  clwwlk0on0  30120  grpodivval  30563  ipval  30731  lnoval  30780  nmoofval  30790  bloval  30809  0ofval  30815  ajfval  30837  hvsubval  31044  hosmval  31763  hommval  31764  hodmval  31765  hfsmval  31766  hfmmval  31767  kbfval  31980  opsqrlem3  32170  dpval  32856  xdivval  32885  smatrcl  33756  smatlem  33757  mdetpmtr12  33785  pstmfval  33856  sxval  34170  ismbfm  34231  dya2iocival  34254  sitgval  34313  sitmval  34330  oddpwdcv  34336  ballotlemgval  34504  vtsval  34630  cvmlift2lem4  35290  icoreval  37335  metf1o  37741  heiborlem3  37799  heiborlem6  37802  heiborlem8  37804  heibor  37807  ldualvs  39118  tendopl  40758  cdlemkuu  40877  dvavsca  40999  dvhvaddval  41072  dvhvscaval  41081  hlhilipval  41935  resubval  42373  prjspnval  42602  rrx2xpref1o  48567  functhinclem1  48840