Theorem ovmpo 7433

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432  (class class class)co 7275   ∈ cmpo 7277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280

This theorem is referenced by:  fvproj  7975  seqomlem1  8281  seqomlem4  8284  oav  8341  omv  8342  oev  8344  iunfictbso  9870  fin23lem12  10087  axdc4lem  10211  axcclem  10213  addpipq2  10692  mulpipq2  10695  subval  11212  divval  11635  cnref1o  12725  ixxval  13087  fzval  13241  modval  13591  om2uzrdg  13676  uzrdgsuci  13680  axdc4uzlem  13703  seqval  13732  seqp1  13736  bcval  14018  cnrecnv  14876  risefacval  15718  fallfacval  15719  gcdval  16203  lcmval  16297  imasvscafn  17248  imasvscaval  17249  grpsubval  18625  isghm  18834  lactghmga  19013  efgmval  19318  efgtval  19329  frgpup3lem  19383  dvrval  19927  frlmval  20955  psrvsca  21160  mat1comp  21589  mamulid  21590  mamurid  21591  madufval  21786  xkococnlem  22810  xkococn  22811  cnextval  23212  dscmet  23728  cncfval  24051  htpycom  24139  htpyid  24140  phtpycom  24151  phtpyid  24152  ehl1eudisval  24585  logbval  25916  isismt  26895  clwwlknon  28454  clwwlk0on0  28456  grpodivval  28897  ipval  29065  lnoval  29114  nmoofval  29124  bloval  29143  0ofval  29149  ajfval  29171  hvsubval  29378  hosmval  30097  hommval  30098  hodmval  30099  hfsmval  30100  hfmmval  30101  kbfval  30314  opsqrlem3  30504  dpval  31164  xdivval  31193  smatrcl  31746  smatlem  31747  mdetpmtr12  31775  pstmfval  31846  sxval  32158  ismbfm  32219  dya2iocival  32240  sitgval  32299  sitmval  32316  oddpwdcv  32322  ballotlemgval  32490  vtsval  32617  cvmlift2lem4  33268  addsval  34126  icoreval  35524  metf1o  35913  heiborlem3  35971  heiborlem6  35974  heiborlem8  35976  heibor  35979  ldualvs  37151  tendopl  38790  cdlemkuu  38909  dvavsca  39031  dvhvaddval  39104  dvhvscaval  39113  hlhilipval  39967  resubval  40350  prjspnval  40455  rrx2xpref1o  46064  functhinclem1  46322