Theorem ovmpo 7579

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3457  (class class class)co 7419   ∈ cmpo 7421

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424

This theorem is used by:  fvproj  8136  seqomlem1  8443  seqomlem4  8446  oav  8502  omv  8503  oev  8505  iunfictbso  10114  fin23lem12  10330  axdc4lem  10454  axcclem  10456  addpipq2  10936  mulpipq2  10939  subval  11463  divval  11889  cnref1o  13025  ixxval  13396  fzval  13553  modval  13922  om2uzrdg  14010  uzrdgsuci  14014  axdc4uzlem  14037  seqval  14066  seqp1  14070  bcval  14358  cnrecnv  15240  risefacval  16085  fallfacval  16086  gcdval  16576  lcmval  16672  imasvscafn  17613  imasvscaval  17614  grpsubval  19096  lactghmga  19519  efgmval  19826  efgtval  19837  frgpup3lem  19891  dvrval  20531  frlmval  21948  psrvsca  22149  mat1comp  22647  mamulid  22648  mamurid  22649  madufval  22844  xkococnlem  23867  xkococn  23868  cnextval  24269  dscmet  24780  cncfval  25098  htpycom  25186  htpyid  25187  phtpycom  25198  phtpyid  25199  ehl1eudisval  25631  logbval  26982  addsval  28206  subsval  28304  mulsval  28353  divsval  28433  seqsval  28532  om2noseqrdg  28548  noseqrdgsuc  28552  seqsp1  28555  expsval  28669  isismt  28854  clwwlknon  30508  clwwlk0on0  30510  grpodivval  30958  ipval  31126  lnoval  31175  nmoofval  31185  bloval  31204  0ofval  31210  ajfval  31232  hvsubval  31439  hosmval  32158  hommval  32159  hodmval  32160  hfsmval  32161  hfmmval  32162  kbfval  32375  opsqrlem3  32565  dpval  33279  xdivval  33308  smatrcl  34250  smatlem  34251  mdetpmtr12  34279  pstmfval  34350  sxval  34645  ismbfm  34706  dya2iocival  34728  sitgval  34787  sitmval  34804  oddpwdcv  34810  ballotlemgval  34979  vtsval  35089  cvmlift2lem4  35835  icoreval  38056  metf1o  38464  heiborlem3  38522  heiborlem6  38525  heiborlem8  38527  heibor  38530  ldualvs  39969  tendopl  41608  cdlemkuu  41727  dvavsca  41849  dvhvaddval  41922  dvhvscaval  41931  hlhilipval  42781  resubval  43186  redivvald  43261  prjspnval  43406  rrx2xpref1o  49555  fuco22natlem  50180  functhinclem1  50279  crosspval  50693