Theorem ovmpo 7593

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480  (class class class)co 7431   ∈ cmpo 7433

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436

This theorem is referenced by:  fvproj  8159  seqomlem1  8490  seqomlem4  8493  oav  8549  omv  8550  oev  8552  iunfictbso  10154  fin23lem12  10371  axdc4lem  10495  axcclem  10497  addpipq2  10976  mulpipq2  10979  subval  11499  divval  11924  cnref1o  13027  ixxval  13395  fzval  13549  modval  13911  om2uzrdg  13997  uzrdgsuci  14001  axdc4uzlem  14024  seqval  14053  seqp1  14057  bcval  14343  cnrecnv  15204  risefacval  16044  fallfacval  16045  gcdval  16533  lcmval  16629  imasvscafn  17582  imasvscaval  17583  grpsubval  19003  isghmOLD  19234  lactghmga  19423  efgmval  19730  efgtval  19741  frgpup3lem  19795  dvrval  20403  frlmval  21768  psrvsca  21969  mat1comp  22446  mamulid  22447  mamurid  22448  madufval  22643  xkococnlem  23667  xkococn  23668  cnextval  24069  dscmet  24585  cncfval  24914  htpycom  25008  htpyid  25009  phtpycom  25020  phtpyid  25021  ehl1eudisval  25455  logbval  26809  addsval  27995  subsval  28090  mulsval  28135  divsval  28215  seqsval  28294  om2noseqrdg  28310  noseqrdgsuc  28314  seqsp1  28317  expsval  28408  isismt  28542  clwwlknon  30109  clwwlk0on0  30111  grpodivval  30554  ipval  30722  lnoval  30771  nmoofval  30781  bloval  30800  0ofval  30806  ajfval  30828  hvsubval  31035  hosmval  31754  hommval  31755  hodmval  31756  hfsmval  31757  hfmmval  31758  kbfval  31971  opsqrlem3  32161  dpval  32872  xdivval  32901  smatrcl  33795  smatlem  33796  mdetpmtr12  33824  pstmfval  33895  sxval  34191  ismbfm  34252  dya2iocival  34275  sitgval  34334  sitmval  34351  oddpwdcv  34357  ballotlemgval  34526  vtsval  34652  cvmlift2lem4  35311  icoreval  37354  metf1o  37762  heiborlem3  37820  heiborlem6  37823  heiborlem8  37825  heibor  37828  ldualvs  39138  tendopl  40778  cdlemkuu  40897  dvavsca  41019  dvhvaddval  41092  dvhvscaval  41101  hlhilipval  41955  resubval  42397  prjspnval  42626  rrx2xpref1o  48639  fuco22natlem  49040  functhinclem1  49093