Theorem ovmpo 7506

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436  (class class class)co 7346   ∈ cmpo 7348

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351

This theorem is referenced by:  fvproj  8064  seqomlem1  8369  seqomlem4  8372  oav  8426  omv  8427  oev  8429  iunfictbso  10005  fin23lem12  10222  axdc4lem  10346  axcclem  10348  addpipq2  10827  mulpipq2  10830  subval  11351  divval  11778  cnref1o  12883  ixxval  13253  fzval  13409  modval  13775  om2uzrdg  13863  uzrdgsuci  13867  axdc4uzlem  13890  seqval  13919  seqp1  13923  bcval  14211  cnrecnv  15072  risefacval  15915  fallfacval  15916  gcdval  16407  lcmval  16503  imasvscafn  17441  imasvscaval  17442  grpsubval  18898  isghmOLD  19128  lactghmga  19317  efgmval  19624  efgtval  19635  frgpup3lem  19689  dvrval  20321  frlmval  21685  psrvsca  21886  mat1comp  22355  mamulid  22356  mamurid  22357  madufval  22552  xkococnlem  23574  xkococn  23575  cnextval  23976  dscmet  24487  cncfval  24808  htpycom  24902  htpyid  24903  phtpycom  24914  phtpyid  24915  ehl1eudisval  25348  logbval  26703  addsval  27905  subsval  28000  mulsval  28048  divsval  28128  seqsval  28218  om2noseqrdg  28234  noseqrdgsuc  28238  seqsp1  28241  expsval  28348  isismt  28512  clwwlknon  30070  clwwlk0on0  30072  grpodivval  30515  ipval  30683  lnoval  30732  nmoofval  30742  bloval  30761  0ofval  30767  ajfval  30789  hvsubval  30996  hosmval  31715  hommval  31716  hodmval  31717  hfsmval  31718  hfmmval  31719  kbfval  31932  opsqrlem3  32122  dpval  32870  xdivval  32899  smatrcl  33809  smatlem  33810  mdetpmtr12  33838  pstmfval  33909  sxval  34203  ismbfm  34264  dya2iocival  34286  sitgval  34345  sitmval  34362  oddpwdcv  34368  ballotlemgval  34537  vtsval  34650  cvmlift2lem4  35350  icoreval  37395  metf1o  37803  heiborlem3  37861  heiborlem6  37864  heiborlem8  37866  heibor  37869  ldualvs  39184  tendopl  40823  cdlemkuu  40942  dvavsca  41064  dvhvaddval  41137  dvhvscaval  41146  hlhilipval  41996  resubval  42408  redivvald  42483  prjspnval  42657  rrx2xpref1o  48758  fuco22natlem  49385  functhinclem1  49484