Theorem ovmpo 7570

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455  (class class class)co 7410   ∈ cmpo 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415

This theorem is referenced by:  fvproj  8126  seqomlem1  8433  seqomlem4  8436  oav  8492  omv  8493  oev  8495  iunfictbso  10094  fin23lem12  10310  axdc4lem  10434  axcclem  10436  addpipq2  10916  mulpipq2  10919  subval  11443  divval  11869  cnref1o  13004  ixxval  13375  fzval  13532  modval  13900  om2uzrdg  13988  uzrdgsuci  13992  axdc4uzlem  14015  seqval  14044  seqp1  14048  bcval  14336  cnrecnv  15212  risefacval  16058  fallfacval  16059  gcdval  16549  lcmval  16645  imasvscafn  17586  imasvscaval  17587  grpsubval  19047  lactghmga  19470  efgmval  19777  efgtval  19788  frgpup3lem  19842  dvrval  20481  frlmval  21898  psrvsca  22099  mat1comp  22597  mamulid  22598  mamurid  22599  madufval  22794  xkococnlem  23816  xkococn  23817  cnextval  24218  dscmet  24729  cncfval  25047  htpycom  25135  htpyid  25136  phtpycom  25147  phtpyid  25148  ehl1eudisval  25580  logbval  26931  addsval  28155  subsval  28253  mulsval  28302  divsval  28382  seqsval  28481  om2noseqrdg  28497  noseqrdgsuc  28501  seqsp1  28504  expsval  28618  isismt  28803  clwwlknon  30441  clwwlk0on0  30443  grpodivval  30887  ipval  31055  lnoval  31104  nmoofval  31114  bloval  31133  0ofval  31139  ajfval  31161  hvsubval  31368  hosmval  32087  hommval  32088  hodmval  32089  hfsmval  32090  hfmmval  32091  kbfval  32304  opsqrlem3  32494  dpval  33209  xdivval  33238  smatrcl  34186  smatlem  34187  mdetpmtr12  34215  pstmfval  34286  sxval  34580  ismbfm  34641  dya2iocival  34663  sitgval  34722  sitmval  34739  oddpwdcv  34745  ballotlemgval  34914  vtsval  35024  cvmlift2lem4  35798  icoreval  37999  metf1o  38406  heiborlem3  38464  heiborlem6  38467  heiborlem8  38469  heibor  38472  ldualvs  39911  tendopl  41550  cdlemkuu  41669  dvavsca  41791  dvhvaddval  41864  dvhvscaval  41873  hlhilipval  42723  resubval  43128  redivvald  43203  prjspnval  43348  rrx2xpref1o  49498  fuco22natlem  50123  functhinclem1  50222