Theorem ovmpo 7578

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3451  (class class class)co 7418   ∈ cmpo 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423

This theorem is used by:  fvproj  8144  seqomlem1  8453  seqomlem4  8456  oav  8512  omv  8513  oev  8515  iunfictbso  10186  fin23lem12  10402  axdc4lem  10526  axcclem  10528  addpipq2  11014  mulpipq2  11017  subval  11541  divval  11969  cnref1o  13106  ixxval  13477  fzval  13634  modval  14004  om2uzrdg  14092  uzrdgsuci  14096  axdc4uzlem  14119  seqval  14148  seqp1  14152  bcval  14441  cnrecnv  15325  risefacval  16168  fallfacval  16169  gcdval  16659  lcmval  16760  imasvscafn  17702  imasvscaval  17703  grpsubval  19189  lactghmga  19612  efgmval  19919  efgtval  19930  frgpup3lem  19984  dvrval  20626  frlmval  22047  psrvsca  22250  mat1comp  22748  mamulid  22749  mamurid  22750  madufval  22945  xkococnlem  23971  xkococn  23972  cnextval  24373  dscmet  24884  cncfval  25202  htpycom  25290  htpyid  25291  phtpycom  25302  phtpyid  25303  ehl1eudisval  25735  logbval  27087  addsval  28341  subsval  28439  mulsval  28488  divsval  28568  seqsval  28667  om2noseqrdg  28683  noseqrdgsuc  28687  seqsp1  28690  expsval  28804  isismt  28990  clwwlknon  30674  clwwlk0on0  30676  grpodivval  31130  ipval  31298  lnoval  31347  nmoofval  31357  bloval  31376  0ofval  31382  ajfval  31404  hvsubval  31611  hosmval  32330  hommval  32331  hodmval  32332  hfsmval  32333  hfmmval  32334  kbfval  32547  opsqrlem3  32737  dpval  33449  xdivval  33478  smatrcl  34421  smatlem  34422  mdetpmtr12  34450  pstmfval  34521  sxval  34816  ismbfm  34877  dya2iocival  34898  sitgval  34957  sitmval  34974  oddpwdcv  34980  ballotlemgval  35149  vtsval  35259  cvmlift2lem4  36050  icoreval  38256  metf1o  38669  heiborlem3  38727  heiborlem6  38730  heiborlem8  38732  heibor  38735  ldualvs  40174  tendopl  41813  cdlemkuu  41932  dvavsca  42054  dvhvaddval  42127  dvhvscaval  42136  hlhilipval  42986  resubval  43398  redivvald  43473  prjspnval  43624  rrx2xpref1o  49799  fuco22natlem  50422  functhinclem1  50521  crosspval  50923