Theorem ovmpo 7612

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454  (class class class)co 7451   ∈ cmpo 7453

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456

This theorem is used by:  fvproj  8188  seqomlem1  8498  seqomlem4  8501  oav  8557  omv  8558  oev  8560  iunfictbso  10232  fin23lem12  10448  axdc4lem  10572  axcclem  10574  addpipq2  11060  mulpipq2  11063  subval  11587  divval  12016  cnref1o  13153  ixxval  13524  fzval  13681  modval  14051  om2uzrdg  14139  uzrdgsuci  14143  axdc4uzlem  14166  seqval  14195  seqp1  14199  bcval  14489  cnrecnv  15375  risefacval  16219  fallfacval  16220  gcdval  16710  lcmval  16811  imasvscafn  17759  imasvscaval  17760  grpsubval  19246  lactghmga  19670  efgmval  19977  efgtval  19988  frgpup3lem  20042  dvrval  20684  frlmval  22109  psrvsca  22312  mat1comp  22810  mamulid  22811  mamurid  22812  madufval  23007  xkococnlem  24033  xkococn  24034  cnextval  24435  dscmet  24946  cncfval  25264  htpycom  25352  htpyid  25353  phtpycom  25364  phtpyid  25365  ehl1eudisval  25797  logbval  27151  addsval  28405  subsval  28503  mulsval  28552  divsval  28632  seqsval  28731  om2noseqrdg  28747  noseqrdgsuc  28751  seqsp1  28754  expsval  28868  isismt  29054  clwwlknon  30738  clwwlk0on0  30740  grpodivval  31194  ipval  31362  lnoval  31411  nmoofval  31421  bloval  31440  0ofval  31446  ajfval  31468  hvsubval  31675  hosmval  32394  hommval  32395  hodmval  32396  hfsmval  32397  hfmmval  32398  kbfval  32611  opsqrlem3  32801  dpval  33552  xdivval  33581  smatrcl  34539  smatlem  34540  mdetpmtr12  34568  pstmfval  34639  sxval  34934  ismbfm  34995  dya2iocival  35016  sitgval  35075  sitmval  35092  oddpwdcv  35098  ballotlemgval  35267  vtsval  35377  cvmlift2lem4  36279  icoreval  38544  metf1o  38955  heiborlem3  39013  heiborlem6  39016  heiborlem8  39018  heibor  39021  ldualvs  40460  tendopl  42099  cdlemkuu  42218  dvavsca  42340  dvhvaddval  42413  dvhvscaval  42422  hlhilipval  43272  resubval  43684  redivvald  43759  prjspnval  43910  fuco22natlem  50798  functhinclem1  50910  crosspval  51382