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 3471  (class class class)co 7424   ∈ cmpo 7426

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 2698  ax-sep 5301  ax-nul 5308  ax-pr 5431

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 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-opab 5213  df-id 5578  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-iota 6503  df-fun 6553  df-fv 6559  df-ov 7427  df-oprab 7428  df-mpo 7429

This theorem is referenced by:  fvproj  8143  seqomlem1  8475  seqomlem4  8478  oav  8536  omv  8537  oev  8539  iunfictbso  10143  fin23lem12  10360  axdc4lem  10484  axcclem  10486  addpipq2  10965  mulpipq2  10968  subval  11487  divval  11910  cnref1o  13005  ixxval  13370  fzval  13524  modval  13874  om2uzrdg  13959  uzrdgsuci  13963  axdc4uzlem  13986  seqval  14015  seqp1  14019  bcval  14301  cnrecnv  15150  risefacval  15990  fallfacval  15991  gcdval  16476  lcmval  16568  imasvscafn  17524  imasvscaval  17525  grpsubval  18947  isghm  19175  lactghmga  19365  efgmval  19672  efgtval  19683  frgpup3lem  19737  dvrval  20347  frlmval  21687  psrvsca  21897  mat1comp  22360  mamulid  22361  mamurid  22362  madufval  22557  xkococnlem  23581  xkococn  23582  cnextval  23983  dscmet  24499  cncfval  24826  htpycom  24920  htpyid  24921  phtpycom  24932  phtpyid  24933  ehl1eudisval  25367  logbval  26716  addsval  27897  subsval  27988  mulsval  28027  divsval  28107  seqsval  28179  om2noseqrdg  28195  noseqrdgsuc  28199  seqsp1  28202  isismt  28356  clwwlknon  29918  clwwlk0on0  29920  grpodivval  30363  ipval  30531  lnoval  30580  nmoofval  30590  bloval  30609  0ofval  30615  ajfval  30637  hvsubval  30844  hosmval  31563  hommval  31564  hodmval  31565  hfsmval  31566  hfmmval  31567  kbfval  31780  opsqrlem3  31970  dpval  32631  xdivval  32660  smatrcl  33402  smatlem  33403  mdetpmtr12  33431  pstmfval  33502  sxval  33814  ismbfm  33875  dya2iocival  33898  sitgval  33957  sitmval  33974  oddpwdcv  33980  ballotlemgval  34148  vtsval  34274  cvmlift2lem4  34921  icoreval  36837  metf1o  37233  heiborlem3  37291  heiborlem6  37294  heiborlem8  37296  heibor  37299  ldualvs  38613  tendopl  40253  cdlemkuu  40372  dvavsca  40494  dvhvaddval  40567  dvhvscaval  40576  hlhilipval  41430  resubval  41925  prjspnval  42043  rrx2xpref1o  47842  functhinclem1  48098

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »