Theorem ovmpo 7509

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3436  (class class class)co 7349   ∈ cmpo 7351

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354

This theorem is referenced by:  fvproj  8067  seqomlem1  8372  seqomlem4  8375  oav  8429  omv  8430  oev  8432  iunfictbso  10008  fin23lem12  10225  axdc4lem  10349  axcclem  10351  addpipq2  10830  mulpipq2  10833  subval  11354  divval  11781  cnref1o  12886  ixxval  13256  fzval  13412  modval  13775  om2uzrdg  13863  uzrdgsuci  13867  axdc4uzlem  13890  seqval  13919  seqp1  13923  bcval  14211  cnrecnv  15072  risefacval  15915  fallfacval  15916  gcdval  16407  lcmval  16503  imasvscafn  17441  imasvscaval  17442  grpsubval  18864  isghmOLD  19095  lactghmga  19284  efgmval  19591  efgtval  19602  frgpup3lem  19656  dvrval  20288  frlmval  21655  psrvsca  21856  mat1comp  22325  mamulid  22326  mamurid  22327  madufval  22522  xkococnlem  23544  xkococn  23545  cnextval  23946  dscmet  24458  cncfval  24779  htpycom  24873  htpyid  24874  phtpycom  24885  phtpyid  24886  ehl1eudisval  25319  logbval  26674  addsval  27874  subsval  27969  mulsval  28017  divsval  28097  seqsval  28187  om2noseqrdg  28203  noseqrdgsuc  28207  seqsp1  28210  expsval  28317  isismt  28479  clwwlknon  30034  clwwlk0on0  30036  grpodivval  30479  ipval  30647  lnoval  30696  nmoofval  30706  bloval  30725  0ofval  30731  ajfval  30753  hvsubval  30960  hosmval  31679  hommval  31680  hodmval  31681  hfsmval  31682  hfmmval  31683  kbfval  31896  opsqrlem3  32086  dpval  32830  xdivval  32859  smatrcl  33763  smatlem  33764  mdetpmtr12  33792  pstmfval  33863  sxval  34157  ismbfm  34218  dya2iocival  34241  sitgval  34300  sitmval  34317  oddpwdcv  34323  ballotlemgval  34492  vtsval  34605  cvmlift2lem4  35279  icoreval  37327  metf1o  37735  heiborlem3  37793  heiborlem6  37796  heiborlem8  37798  heibor  37801  ldualvs  39116  tendopl  40755  cdlemkuu  40874  dvavsca  40996  dvhvaddval  41069  dvhvscaval  41078  hlhilipval  41928  resubval  42340  redivvald  42415  prjspnval  42589  rrx2xpref1o  48703  fuco22natlem  49330  functhinclem1  49429