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

Theorem ovmpt2 6215
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  |-  ( x  =  A  ->  R  =  G )
ovmpt2g.2  |-  ( y  =  B  ->  G  =  S )
ovmpt2g.3  |-  F  =  ( x  e.  C ,  y  e.  D  |->  R )
ovmpt2.4  |-  S  e. 
_V
Assertion
Ref Expression
ovmpt2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Distinct variable groups:    x, y, A    x, B, y    x, C, y    x, D, y   
x, S, y
Allowed substitution hints:    R( x, y)    F( x, y)    G( x, y)

Proof of Theorem ovmpt2
StepHypRef Expression
1 ovmpt2.4 . 2  |-  S  e. 
_V
2 ovmpt2g.1 . . 3  |-  ( x  =  A  ->  R  =  G )
3 ovmpt2g.2 . . 3  |-  ( y  =  B  ->  G  =  S )
4 ovmpt2g.3 . . 3  |-  F  =  ( x  e.  C ,  y  e.  D  |->  R )
52, 3, 4ovmpt2g 6214 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  S  e.  _V )  ->  ( A F B )  =  S )
61, 5mp3an3 1296 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362    e. wcel 1755   _Vcvv 2962  (class class class)co 6080    e. cmpt2 6082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-iota 5369  df-fun 5408  df-fv 5414  df-ov 6083  df-oprab 6084  df-mpt2 6085
This theorem is referenced by:  seqomlem1  6891  seqomlem4  6894  oav  6939  omv  6940  oev  6942  iunfictbso  8272  fin23lem12  8488  axdc4lem  8612  axcclem  8614  addpipq2  9093  mulpipq2  9096  subval  9589  divval  9984  cnref1o  10974  ixxval  11296  fzval  11426  modval  11694  om2uzrdg  11763  uzrdgsuci  11767  axdc4uzlem  11788  seqval  11801  seqp1  11805  bcval  12064  cnrecnv  12638  gcdval  13675  imasvscafn  14458  imasvscaval  14459  grpsubval  15561  isghm  15727  lactghmga  15889  efgmval  16189  efgtval  16200  frgpup3lem  16254  dvrval  16711  psrvsca  17396  frlmval  18015  dmatcomp  18145  mamulid  18146  mamurid  18147  madufval  18285  xkococnlem  19074  xkococn  19075  cnextval  19475  dscmet  20007  cncfval  20306  htpycom  20390  htpyid  20391  phtpycom  20402  phtpyid  20403  grpodivval  23553  gxval  23568  ipval  23921  lnoval  23975  nmoofval  23985  bloval  24004  0ofval  24010  ajfval  24032  hvsubval  24241  hosmval  24962  hommval  24963  hodmval  24964  hfsmval  24965  hfmmval  24966  kbfval  25179  opsqrlem3  25369  xdivval  25917  pstmfval  26177  logbval  26305  sxval  26458  ismbfm  26521  dya2iocival  26542  sitgval  26566  sitmval  26582  oddpwdcv  26586  ballotlemgval  26754  cvmlift2lem4  27043  elgiso  27162  risefacval  27358  fallfacval  27359  metf1o  28495  heiborlem3  28556  heiborlem6  28559  heiborlem8  28561  heibor  28564  dpval  30835  ldualvs  32376  tendopl  34014  cdlemkuu  34133  dvavsca  34255  dvhvaddval  34329  dvhvscaval  34338  hlhilipval  35191
  Copyright terms: Public domain W3C validator