Theorem ovmpo 7565

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3459  (class class class)co 7403   ∈ cmpo 7405

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6483  df-fun 6532  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408

This theorem is referenced by:  fvproj  8131  seqomlem1  8462  seqomlem4  8465  oav  8521  omv  8522  oev  8524  iunfictbso  10126  fin23lem12  10343  axdc4lem  10467  axcclem  10469  addpipq2  10948  mulpipq2  10951  subval  11471  divval  11896  cnref1o  12999  ixxval  13368  fzval  13524  modval  13886  om2uzrdg  13972  uzrdgsuci  13976  axdc4uzlem  13999  seqval  14028  seqp1  14032  bcval  14320  cnrecnv  15182  risefacval  16022  fallfacval  16023  gcdval  16513  lcmval  16609  imasvscafn  17549  imasvscaval  17550  grpsubval  18966  isghmOLD  19197  lactghmga  19384  efgmval  19691  efgtval  19702  frgpup3lem  19756  dvrval  20361  frlmval  21706  psrvsca  21907  mat1comp  22376  mamulid  22377  mamurid  22378  madufval  22573  xkococnlem  23595  xkococn  23596  cnextval  23997  dscmet  24509  cncfval  24830  htpycom  24924  htpyid  24925  phtpycom  24936  phtpyid  24937  ehl1eudisval  25371  logbval  26726  addsval  27912  subsval  28007  mulsval  28052  divsval  28132  seqsval  28211  om2noseqrdg  28227  noseqrdgsuc  28231  seqsp1  28234  expsval  28325  isismt  28459  clwwlknon  30017  clwwlk0on0  30019  grpodivval  30462  ipval  30630  lnoval  30679  nmoofval  30689  bloval  30708  0ofval  30714  ajfval  30736  hvsubval  30943  hosmval  31662  hommval  31663  hodmval  31664  hfsmval  31665  hfmmval  31666  kbfval  31879  opsqrlem3  32069  dpval  32810  xdivval  32839  smatrcl  33773  smatlem  33774  mdetpmtr12  33802  pstmfval  33873  sxval  34167  ismbfm  34228  dya2iocival  34251  sitgval  34310  sitmval  34327  oddpwdcv  34333  ballotlemgval  34502  vtsval  34615  cvmlift2lem4  35274  icoreval  37317  metf1o  37725  heiborlem3  37783  heiborlem6  37786  heiborlem8  37788  heibor  37791  ldualvs  39101  tendopl  40741  cdlemkuu  40860  dvavsca  40982  dvhvaddval  41055  dvhvscaval  41064  hlhilipval  41914  resubval  42357  prjspnval  42586  rrx2xpref1o  48646  fuco22natlem  49204  functhinclem1  49278