Theorem ovmpo 7571

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3463  (class class class)co 7411   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  fvproj  8129  seqomlem1  8436  seqomlem4  8439  oav  8495  omv  8496  oev  8498  iunfictbso  10097  fin23lem12  10314  axdc4lem  10438  axcclem  10440  addpipq2  10920  mulpipq2  10923  subval  11447  divval  11873  cnref1o  13008  ixxval  13379  fzval  13536  modval  13903  om2uzrdg  13991  uzrdgsuci  13995  axdc4uzlem  14018  seqval  14047  seqp1  14051  bcval  14339  cnrecnv  15215  risefacval  16061  fallfacval  16062  gcdval  16553  lcmval  16649  imasvscafn  17590  imasvscaval  17591  grpsubval  19051  lactghmga  19474  efgmval  19781  efgtval  19792  frgpup3lem  19846  dvrval  20484  frlmval  21866  psrvsca  22067  mat1comp  22565  mamulid  22566  mamurid  22567  madufval  22762  xkococnlem  23784  xkococn  23785  cnextval  24186  dscmet  24697  cncfval  25015  htpycom  25103  htpyid  25104  phtpycom  25115  phtpyid  25116  ehl1eudisval  25548  logbval  26896  addsval  28120  subsval  28218  mulsval  28267  divsval  28347  seqsval  28446  om2noseqrdg  28462  noseqrdgsuc  28466  seqsp1  28469  expsval  28583  isismt  28768  clwwlknon  30381  clwwlk0on0  30383  grpodivval  30827  ipval  30995  lnoval  31044  nmoofval  31054  bloval  31073  0ofval  31079  ajfval  31101  hvsubval  31308  hosmval  32027  hommval  32028  hodmval  32029  hfsmval  32030  hfmmval  32031  kbfval  32244  opsqrlem3  32434  dpval  33149  xdivval  33178  smatrcl  34130  smatlem  34131  mdetpmtr12  34159  pstmfval  34230  sxval  34524  ismbfm  34585  dya2iocival  34607  sitgval  34666  sitmval  34683  oddpwdcv  34689  ballotlemgval  34858  vtsval  34968  cvmlift2lem4  35696  icoreval  37886  metf1o  38293  heiborlem3  38351  heiborlem6  38354  heiborlem8  38356  heibor  38359  ldualvs  39800  tendopl  41439  cdlemkuu  41558  dvavsca  41680  dvhvaddval  41753  dvhvscaval  41762  hlhilipval  42612  resubval  43017  redivvald  43092  prjspnval  43239  rrx2xpref1o  49382  fuco22natlem  50007  functhinclem1  50106