Theorem ovmpo 7516

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3438  (class class class)co 7356   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-iota 6446  df-fun 6492  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  fvproj  8074  seqomlem1  8379  seqomlem4  8382  oav  8436  omv  8437  oev  8439  iunfictbso  10022  fin23lem12  10239  axdc4lem  10363  axcclem  10365  addpipq2  10845  mulpipq2  10848  subval  11369  divval  11796  cnref1o  12896  ixxval  13267  fzval  13423  modval  13789  om2uzrdg  13877  uzrdgsuci  13881  axdc4uzlem  13904  seqval  13933  seqp1  13937  bcval  14225  cnrecnv  15086  risefacval  15929  fallfacval  15930  gcdval  16421  lcmval  16517  imasvscafn  17456  imasvscaval  17457  grpsubval  18913  isghmOLD  19143  lactghmga  19332  efgmval  19639  efgtval  19650  frgpup3lem  19704  dvrval  20337  frlmval  21701  psrvsca  21903  mat1comp  22382  mamulid  22383  mamurid  22384  madufval  22579  xkococnlem  23601  xkococn  23602  cnextval  24003  dscmet  24514  cncfval  24835  htpycom  24929  htpyid  24930  phtpycom  24941  phtpyid  24942  ehl1eudisval  25375  logbval  26730  addsval  27932  subsval  28029  mulsval  28078  divsval  28158  seqsval  28249  om2noseqrdg  28265  noseqrdgsuc  28269  seqsp1  28272  expsval  28383  isismt  28555  clwwlknon  30114  clwwlk0on0  30116  grpodivval  30559  ipval  30727  lnoval  30776  nmoofval  30786  bloval  30805  0ofval  30811  ajfval  30833  hvsubval  31040  hosmval  31759  hommval  31760  hodmval  31761  hfsmval  31762  hfmmval  31763  kbfval  31976  opsqrlem3  32166  dpval  32920  xdivval  32949  smatrcl  33902  smatlem  33903  mdetpmtr12  33931  pstmfval  34002  sxval  34296  ismbfm  34357  dya2iocival  34379  sitgval  34438  sitmval  34455  oddpwdcv  34461  ballotlemgval  34630  vtsval  34743  cvmlift2lem4  35449  icoreval  37497  metf1o  37895  heiborlem3  37953  heiborlem6  37956  heiborlem8  37958  heibor  37961  ldualvs  39336  tendopl  40975  cdlemkuu  41094  dvavsca  41216  dvhvaddval  41289  dvhvscaval  41298  hlhilipval  42148  resubval  42564  redivvald  42639  prjspnval  42801  rrx2xpref1o  48906  fuco22natlem  49532  functhinclem1  49631