Theorem ovmpo 7310

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  Vcvv 3494  (class class class)co 7156   ∈ cmpo 7158

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161

This theorem is referenced by:  fvproj  7828  seqomlem1  8086  seqomlem4  8089  oav  8136  omv  8137  oev  8139  iunfictbso  9540  fin23lem12  9753  axdc4lem  9877  axcclem  9879  addpipq2  10358  mulpipq2  10361  subval  10877  divval  11300  cnref1o  12385  ixxval  12747  fzval  12895  modval  13240  om2uzrdg  13325  uzrdgsuci  13329  axdc4uzlem  13352  seqval  13381  seqp1  13385  bcval  13665  cnrecnv  14524  risefacval  15362  fallfacval  15363  gcdval  15845  lcmval  15936  imasvscafn  16810  imasvscaval  16811  grpsubval  18149  isghm  18358  lactghmga  18533  efgmval  18838  efgtval  18849  frgpup3lem  18903  dvrval  19435  psrvsca  20171  frlmval  20892  mat1comp  21049  mamulid  21050  mamurid  21051  madufval  21246  xkococnlem  22267  xkococn  22268  cnextval  22669  dscmet  23182  cncfval  23496  htpycom  23580  htpyid  23581  phtpycom  23592  phtpyid  23593  ehl1eudisval  24024  logbval  25344  isismt  26320  clwwlknon  27869  clwwlk0on0  27871  grpodivval  28312  ipval  28480  lnoval  28529  nmoofval  28539  bloval  28558  0ofval  28564  ajfval  28586  hvsubval  28793  hosmval  29512  hommval  29513  hodmval  29514  hfsmval  29515  hfmmval  29516  kbfval  29729  opsqrlem3  29919  dpval  30566  xdivval  30595  smatrcl  31061  smatlem  31062  mdetpmtr12  31090  pstmfval  31136  sxval  31449  ismbfm  31510  dya2iocival  31531  sitgval  31590  sitmval  31607  oddpwdcv  31613  ballotlemgval  31781  vtsval  31908  cvmlift2lem4  32553  icoreval  34637  metf1o  35045  heiborlem3  35106  heiborlem6  35109  heiborlem8  35111  heibor  35114  ldualvs  36288  tendopl  37927  cdlemkuu  38046  dvavsca  38168  dvhvaddval  38241  dvhvscaval  38250  hlhilipval  39100  resubval  39217  prjspnval  39286  rrx2xpref1o  44725