Theorem ovmpo 7567

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474  (class class class)co 7408   ∈ cmpo 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413

This theorem is referenced by:  fvproj  8119  seqomlem1  8449  seqomlem4  8452  oav  8510  omv  8511  oev  8513  iunfictbso  10108  fin23lem12  10325  axdc4lem  10449  axcclem  10451  addpipq2  10930  mulpipq2  10933  subval  11450  divval  11873  cnref1o  12968  ixxval  13331  fzval  13485  modval  13835  om2uzrdg  13920  uzrdgsuci  13924  axdc4uzlem  13947  seqval  13976  seqp1  13980  bcval  14263  cnrecnv  15111  risefacval  15951  fallfacval  15952  gcdval  16436  lcmval  16528  imasvscafn  17482  imasvscaval  17483  grpsubval  18869  isghm  19091  lactghmga  19272  efgmval  19579  efgtval  19590  frgpup3lem  19644  dvrval  20216  frlmval  21302  psrvsca  21509  mat1comp  21941  mamulid  21942  mamurid  21943  madufval  22138  xkococnlem  23162  xkococn  23163  cnextval  23564  dscmet  24080  cncfval  24403  htpycom  24491  htpyid  24492  phtpycom  24503  phtpyid  24504  ehl1eudisval  24937  logbval  26268  addsval  27443  subsval  27529  mulsval  27562  divsval  27634  isismt  27782  clwwlknon  29340  clwwlk0on0  29342  grpodivval  29783  ipval  29951  lnoval  30000  nmoofval  30010  bloval  30029  0ofval  30035  ajfval  30057  hvsubval  30264  hosmval  30983  hommval  30984  hodmval  30985  hfsmval  30986  hfmmval  30987  kbfval  31200  opsqrlem3  31390  dpval  32051  xdivval  32080  smatrcl  32771  smatlem  32772  mdetpmtr12  32800  pstmfval  32871  sxval  33183  ismbfm  33244  dya2iocival  33267  sitgval  33326  sitmval  33343  oddpwdcv  33349  ballotlemgval  33517  vtsval  33644  cvmlift2lem4  34292  icoreval  36229  metf1o  36618  heiborlem3  36676  heiborlem6  36679  heiborlem8  36681  heibor  36684  ldualvs  38002  tendopl  39642  cdlemkuu  39761  dvavsca  39883  dvhvaddval  39956  dvhvscaval  39965  hlhilipval  40819  resubval  41241  prjspnval  41359  rrx2xpref1o  47394  functhinclem1  47651