Theorem ovmpo 7518

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

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

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363

This theorem is referenced by:  fvproj  8076  seqomlem1  8381  seqomlem4  8384  oav  8438  omv  8439  oev  8441  iunfictbso  10024  fin23lem12  10241  axdc4lem  10365  axcclem  10367  addpipq2  10847  mulpipq2  10850  subval  11371  divval  11798  cnref1o  12898  ixxval  13269  fzval  13425  modval  13791  om2uzrdg  13879  uzrdgsuci  13883  axdc4uzlem  13906  seqval  13935  seqp1  13939  bcval  14227  cnrecnv  15088  risefacval  15931  fallfacval  15932  gcdval  16423  lcmval  16519  imasvscafn  17458  imasvscaval  17459  grpsubval  18915  isghmOLD  19145  lactghmga  19334  efgmval  19641  efgtval  19652  frgpup3lem  19706  dvrval  20339  frlmval  21703  psrvsca  21905  mat1comp  22384  mamulid  22385  mamurid  22386  madufval  22581  xkococnlem  23603  xkococn  23604  cnextval  24005  dscmet  24516  cncfval  24837  htpycom  24931  htpyid  24932  phtpycom  24943  phtpyid  24944  ehl1eudisval  25377  logbval  26732  addsval  27958  subsval  28056  mulsval  28105  divsval  28185  seqsval  28284  om2noseqrdg  28300  noseqrdgsuc  28304  seqsp1  28307  expsval  28421  isismt  28606  clwwlknon  30165  clwwlk0on0  30167  grpodivval  30610  ipval  30778  lnoval  30827  nmoofval  30837  bloval  30856  0ofval  30862  ajfval  30884  hvsubval  31091  hosmval  31810  hommval  31811  hodmval  31812  hfsmval  31813  hfmmval  31814  kbfval  32027  opsqrlem3  32217  dpval  32971  xdivval  33000  smatrcl  33953  smatlem  33954  mdetpmtr12  33982  pstmfval  34053  sxval  34347  ismbfm  34408  dya2iocival  34430  sitgval  34489  sitmval  34506  oddpwdcv  34512  ballotlemgval  34681  vtsval  34794  cvmlift2lem4  35500  icoreval  37558  metf1o  37956  heiborlem3  38014  heiborlem6  38017  heiborlem8  38019  heibor  38022  ldualvs  39397  tendopl  41036  cdlemkuu  41155  dvavsca  41277  dvhvaddval  41350  dvhvscaval  41359  hlhilipval  42209  resubval  42622  redivvald  42697  prjspnval  42859  rrx2xpref1o  48964  fuco22natlem  49590  functhinclem1  49689