Theorem ovmpo 7568

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475  (class class class)co 7409   ∈ cmpo 7411

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414

This theorem is referenced by:  fvproj  8120  seqomlem1  8450  seqomlem4  8453  oav  8511  omv  8512  oev  8514  iunfictbso  10109  fin23lem12  10326  axdc4lem  10450  axcclem  10452  addpipq2  10931  mulpipq2  10934  subval  11451  divval  11874  cnref1o  12969  ixxval  13332  fzval  13486  modval  13836  om2uzrdg  13921  uzrdgsuci  13925  axdc4uzlem  13948  seqval  13977  seqp1  13981  bcval  14264  cnrecnv  15112  risefacval  15952  fallfacval  15953  gcdval  16437  lcmval  16529  imasvscafn  17483  imasvscaval  17484  grpsubval  18870  isghm  19092  lactghmga  19273  efgmval  19580  efgtval  19591  frgpup3lem  19645  dvrval  20217  frlmval  21303  psrvsca  21510  mat1comp  21942  mamulid  21943  mamurid  21944  madufval  22139  xkococnlem  23163  xkococn  23164  cnextval  23565  dscmet  24081  cncfval  24404  htpycom  24492  htpyid  24493  phtpycom  24504  phtpyid  24505  ehl1eudisval  24938  logbval  26271  addsval  27446  subsval  27532  mulsval  27565  divsval  27637  isismt  27785  clwwlknon  29343  clwwlk0on0  29345  grpodivval  29788  ipval  29956  lnoval  30005  nmoofval  30015  bloval  30034  0ofval  30040  ajfval  30062  hvsubval  30269  hosmval  30988  hommval  30989  hodmval  30990  hfsmval  30991  hfmmval  30992  kbfval  31205  opsqrlem3  31395  dpval  32056  xdivval  32085  smatrcl  32776  smatlem  32777  mdetpmtr12  32805  pstmfval  32876  sxval  33188  ismbfm  33249  dya2iocival  33272  sitgval  33331  sitmval  33348  oddpwdcv  33354  ballotlemgval  33522  vtsval  33649  cvmlift2lem4  34297  icoreval  36234  metf1o  36623  heiborlem3  36681  heiborlem6  36684  heiborlem8  36686  heibor  36689  ldualvs  38007  tendopl  39647  cdlemkuu  39766  dvavsca  39888  dvhvaddval  39961  dvhvscaval  39970  hlhilipval  40824  resubval  41240  prjspnval  41358  rrx2xpref1o  47404  functhinclem1  47661