Theorem ovmpo 7585

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  Vcvv 3461  (class class class)co 7423   ∈ cmpo 7425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3776  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-iota 6505  df-fun 6555  df-fv 6561  df-ov 7426  df-oprab 7427  df-mpo 7428

This theorem is referenced by:  fvproj  8147  seqomlem1  8479  seqomlem4  8482  oav  8540  omv  8541  oev  8543  iunfictbso  10153  fin23lem12  10370  axdc4lem  10494  axcclem  10496  addpipq2  10975  mulpipq2  10978  subval  11497  divval  11921  cnref1o  13016  ixxval  13381  fzval  13535  modval  13886  om2uzrdg  13971  uzrdgsuci  13975  axdc4uzlem  13998  seqval  14027  seqp1  14031  bcval  14316  cnrecnv  15165  risefacval  16005  fallfacval  16006  gcdval  16491  lcmval  16588  imasvscafn  17547  imasvscaval  17548  grpsubval  18975  isghmOLD  19205  lactghmga  19398  efgmval  19705  efgtval  19716  frgpup3lem  19770  dvrval  20380  frlmval  21738  psrvsca  21950  mat1comp  22425  mamulid  22426  mamurid  22427  madufval  22622  xkococnlem  23646  xkococn  23647  cnextval  24048  dscmet  24564  cncfval  24891  htpycom  24985  htpyid  24986  phtpycom  24997  phtpyid  24998  ehl1eudisval  25432  logbval  26786  addsval  27968  subsval  28059  mulsval  28102  divsval  28182  seqsval  28254  om2noseqrdg  28270  noseqrdgsuc  28274  seqsp1  28277  isismt  28453  clwwlknon  30015  clwwlk0on0  30017  grpodivval  30460  ipval  30628  lnoval  30677  nmoofval  30687  bloval  30706  0ofval  30712  ajfval  30734  hvsubval  30941  hosmval  31660  hommval  31661  hodmval  31662  hfsmval  31663  hfmmval  31664  kbfval  31877  opsqrlem3  32067  dpval  32740  xdivval  32769  smatrcl  33567  smatlem  33568  mdetpmtr12  33596  pstmfval  33667  sxval  33979  ismbfm  34040  dya2iocival  34063  sitgval  34122  sitmval  34139  oddpwdcv  34145  ballotlemgval  34313  vtsval  34439  cvmlift2lem4  35086  icoreval  37008  metf1o  37404  heiborlem3  37462  heiborlem6  37465  heiborlem8  37467  heibor  37470  ldualvs  38783  tendopl  40423  cdlemkuu  40542  dvavsca  40664  dvhvaddval  40737  dvhvscaval  40746  hlhilipval  41600  resubval  42089  prjspnval  42207  rrx2xpref1o  48043  functhinclem1  48299