Theorem ovmpo 7529

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3444  (class class class)co 7369   ∈ cmpo 7371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374

This theorem is referenced by:  fvproj  8090  seqomlem1  8395  seqomlem4  8398  oav  8452  omv  8453  oev  8455  iunfictbso  10043  fin23lem12  10260  axdc4lem  10384  axcclem  10386  addpipq2  10865  mulpipq2  10868  subval  11388  divval  11815  cnref1o  12920  ixxval  13290  fzval  13446  modval  13809  om2uzrdg  13897  uzrdgsuci  13901  axdc4uzlem  13924  seqval  13953  seqp1  13957  bcval  14245  cnrecnv  15107  risefacval  15950  fallfacval  15951  gcdval  16442  lcmval  16538  imasvscafn  17476  imasvscaval  17477  grpsubval  18899  isghmOLD  19130  lactghmga  19319  efgmval  19626  efgtval  19637  frgpup3lem  19691  dvrval  20323  frlmval  21690  psrvsca  21891  mat1comp  22360  mamulid  22361  mamurid  22362  madufval  22557  xkococnlem  23579  xkococn  23580  cnextval  23981  dscmet  24493  cncfval  24814  htpycom  24908  htpyid  24909  phtpycom  24920  phtpyid  24921  ehl1eudisval  25354  logbval  26709  addsval  27909  subsval  28004  mulsval  28052  divsval  28132  seqsval  28222  om2noseqrdg  28238  noseqrdgsuc  28242  seqsp1  28245  expsval  28352  isismt  28514  clwwlknon  30069  clwwlk0on0  30071  grpodivval  30514  ipval  30682  lnoval  30731  nmoofval  30741  bloval  30760  0ofval  30766  ajfval  30788  hvsubval  30995  hosmval  31714  hommval  31715  hodmval  31716  hfsmval  31717  hfmmval  31718  kbfval  31931  opsqrlem3  32121  dpval  32860  xdivval  32889  smatrcl  33779  smatlem  33780  mdetpmtr12  33808  pstmfval  33879  sxval  34173  ismbfm  34234  dya2iocival  34257  sitgval  34316  sitmval  34333  oddpwdcv  34339  ballotlemgval  34508  vtsval  34621  cvmlift2lem4  35286  icoreval  37334  metf1o  37742  heiborlem3  37800  heiborlem6  37803  heiborlem8  37805  heibor  37808  ldualvs  39123  tendopl  40763  cdlemkuu  40882  dvavsca  41004  dvhvaddval  41077  dvhvscaval  41086  hlhilipval  41936  resubval  42348  redivvald  42423  prjspnval  42597  rrx2xpref1o  48700  fuco22natlem  49327  functhinclem1  49426