Theorem ovmpo 7551

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450  (class class class)co 7389   ∈ cmpo 7391

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 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-iota 6466  df-fun 6515  df-fv 6521  df-ov 7392  df-oprab 7393  df-mpo 7394

This theorem is referenced by:  fvproj  8115  seqomlem1  8420  seqomlem4  8423  oav  8477  omv  8478  oev  8480  iunfictbso  10073  fin23lem12  10290  axdc4lem  10414  axcclem  10416  addpipq2  10895  mulpipq2  10898  subval  11418  divval  11845  cnref1o  12950  ixxval  13320  fzval  13476  modval  13839  om2uzrdg  13927  uzrdgsuci  13931  axdc4uzlem  13954  seqval  13983  seqp1  13987  bcval  14275  cnrecnv  15137  risefacval  15980  fallfacval  15981  gcdval  16472  lcmval  16568  imasvscafn  17506  imasvscaval  17507  grpsubval  18923  isghmOLD  19154  lactghmga  19341  efgmval  19648  efgtval  19659  frgpup3lem  19713  dvrval  20318  frlmval  21663  psrvsca  21864  mat1comp  22333  mamulid  22334  mamurid  22335  madufval  22530  xkococnlem  23552  xkococn  23553  cnextval  23954  dscmet  24466  cncfval  24787  htpycom  24881  htpyid  24882  phtpycom  24893  phtpyid  24894  ehl1eudisval  25327  logbval  26682  addsval  27875  subsval  27970  mulsval  28018  divsval  28098  seqsval  28188  om2noseqrdg  28204  noseqrdgsuc  28208  seqsp1  28211  expsval  28317  isismt  28467  clwwlknon  30025  clwwlk0on0  30027  grpodivval  30470  ipval  30638  lnoval  30687  nmoofval  30697  bloval  30716  0ofval  30722  ajfval  30744  hvsubval  30951  hosmval  31670  hommval  31671  hodmval  31672  hfsmval  31673  hfmmval  31674  kbfval  31887  opsqrlem3  32077  dpval  32816  xdivval  32845  smatrcl  33792  smatlem  33793  mdetpmtr12  33821  pstmfval  33892  sxval  34186  ismbfm  34247  dya2iocival  34270  sitgval  34329  sitmval  34346  oddpwdcv  34352  ballotlemgval  34521  vtsval  34634  cvmlift2lem4  35293  icoreval  37336  metf1o  37744  heiborlem3  37802  heiborlem6  37805  heiborlem8  37807  heibor  37810  ldualvs  39125  tendopl  40765  cdlemkuu  40884  dvavsca  41006  dvhvaddval  41079  dvhvscaval  41088  hlhilipval  41938  resubval  42350  redivvald  42425  prjspnval  42597  rrx2xpref1o  48697  fuco22natlem  49324  functhinclem1  49423