MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovmpt2 Structured version   Visualization version   GIF version

Theorem ovmpt2 6994
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
ovmpt2g.1 (𝑥 = 𝐴𝑅 = 𝐺)
ovmpt2g.2 (𝑦 = 𝐵𝐺 = 𝑆)
ovmpt2g.3 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
ovmpt2.4 𝑆 ∈ V
Assertion
Ref Expression
ovmpt2 ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem ovmpt2
StepHypRef Expression
1 ovmpt2.4 . 2 𝑆 ∈ V
2 ovmpt2g.1 . . 3 (𝑥 = 𝐴𝑅 = 𝐺)
3 ovmpt2g.2 . . 3 (𝑦 = 𝐵𝐺 = 𝑆)
4 ovmpt2g.3 . . 3 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
52, 3, 4ovmpt2g 6993 . 2 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
61, 5mp3an3 1574 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  Vcvv 3350  (class class class)co 6842  cmpt2 6844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-iota 6031  df-fun 6070  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847
This theorem is referenced by:  seqomlem1  7749  seqomlem4  7752  oav  7796  omv  7797  oev  7799  iunfictbso  9188  fin23lem12  9406  axdc4lem  9530  axcclem  9532  addpipq2  10011  mulpipq2  10014  subval  10526  divval  10941  cnref1o  12023  ixxval  12385  fzval  12535  modval  12878  om2uzrdg  12963  uzrdgsuci  12967  axdc4uzlem  12990  seqval  13019  seqp1  13023  bcval  13295  cnrecnv  14190  risefacval  15021  fallfacval  15022  gcdval  15499  lcmval  15586  imasvscafn  16463  imasvscaval  16464  grpsubval  17732  isghm  17924  lactghmga  18087  efgmval  18389  efgtval  18400  frgpup3lem  18456  dvrval  18952  psrvsca  19665  frlmval  20368  mat1comp  20522  mamulid  20523  mamurid  20524  madufval  20720  xkococnlem  21742  xkococn  21743  cnextval  22144  dscmet  22656  cncfval  22970  htpycom  23054  htpyid  23055  phtpycom  23066  phtpyid  23067  logbval  24795  isismt  25720  clwwlknon  27360  clwwlknonOLD  27361  clwwlk0on0  27364  grpodivval  27846  ipval  28014  lnoval  28063  nmoofval  28073  bloval  28092  0ofval  28098  ajfval  28120  hvsubval  28329  hosmval  29050  hommval  29051  hodmval  29052  hfsmval  29053  hfmmval  29054  kbfval  29267  opsqrlem3  29457  dpval  30045  xdivval  30074  smatrcl  30309  smatlem  30310  mdetpmtr12  30338  fvproj  30346  pstmfval  30386  sxval  30700  ismbfm  30761  dya2iocival  30782  sitgval  30841  sitmval  30858  oddpwdcv  30864  ballotlemgval  31033  vtsval  31166  cvmlift2lem4  31736  icoreval  33634  metf1o  33973  heiborlem3  34034  heiborlem6  34037  heiborlem8  34039  heibor  34042  ldualvs  35093  tendopl  36732  cdlemkuu  36851  dvavsca  36973  dvhvaddval  37046  dvhvscaval  37055  hlhilipval  37905
  Copyright terms: Public domain W3C validator