Theorem ovmpo 7556

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  Vcvv 3454  (class class class)co 7396   ∈ cmpo 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-iota 6477  df-fun 6523  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401

This theorem is referenced by:  fvproj  8114  seqomlem1  8421  seqomlem4  8424  oav  8480  omv  8481  oev  8483  iunfictbso  10070  fin23lem12  10288  axdc4lem  10412  axcclem  10414  addpipq2  10894  mulpipq2  10897  subval  11421  divval  11847  cnref1o  12986  ixxval  13357  fzval  13514  modval  13881  om2uzrdg  13969  uzrdgsuci  13973  axdc4uzlem  13996  seqval  14025  seqp1  14029  bcval  14317  cnrecnv  15192  risefacval  16038  fallfacval  16039  gcdval  16530  lcmval  16626  imasvscafn  17567  imasvscaval  17568  grpsubval  19027  lactghmga  19445  efgmval  19752  efgtval  19763  frgpup3lem  19817  dvrval  20448  frlmval  21797  psrvsca  21998  mat1comp  22497  mamulid  22498  mamurid  22499  madufval  22694  xkococnlem  23716  xkococn  23717  cnextval  24118  dscmet  24629  cncfval  24947  htpycom  25035  htpyid  25036  phtpycom  25047  phtpyid  25048  ehl1eudisval  25480  logbval  26828  addsval  28052  subsval  28150  mulsval  28199  divsval  28279  seqsval  28378  om2noseqrdg  28394  noseqrdgsuc  28398  seqsp1  28401  expsval  28515  isismt  28700  clwwlknon  30289  clwwlk0on0  30291  grpodivval  30735  ipval  30903  lnoval  30952  nmoofval  30962  bloval  30981  0ofval  30987  ajfval  31009  hvsubval  31216  hosmval  31935  hommval  31936  hodmval  31937  hfsmval  31938  hfmmval  31939  kbfval  32152  opsqrlem3  32342  dpval  33064  xdivval  33093  smatrcl  34090  smatlem  34091  mdetpmtr12  34119  pstmfval  34190  sxval  34484  ismbfm  34545  dya2iocival  34567  sitgval  34626  sitmval  34643  oddpwdcv  34649  ballotlemgval  34818  vtsval  34928  cvmlift2lem4  35653  icoreval  37844  metf1o  38251  heiborlem3  38309  heiborlem6  38312  heiborlem8  38314  heibor  38317  ldualvs  39758  tendopl  41397  cdlemkuu  41516  dvavsca  41638  dvhvaddval  41711  dvhvscaval  41720  hlhilipval  42570  resubval  42973  redivvald  43048  prjspnval  43195  rrx2xpref1o  49337  fuco22natlem  49963  functhinclem1  50062