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

Theorem ovmpt2 6422
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 6421 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  S  e.  _V )  ->  ( A F B )  =  S )
61, 5mp3an3 1313 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   _Vcvv 3113  (class class class)co 6284    |-> cmpt2 6286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5551  df-fun 5590  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289
This theorem is referenced by:  seqomlem1  7115  seqomlem4  7118  oav  7161  omv  7162  oev  7164  iunfictbso  8495  fin23lem12  8711  axdc4lem  8835  axcclem  8837  addpipq2  9314  mulpipq2  9317  subval  9811  divval  10209  cnref1o  11215  ixxval  11537  fzval  11674  modval  11966  om2uzrdg  12035  uzrdgsuci  12039  axdc4uzlem  12060  seqval  12086  seqp1  12090  bcval  12350  cnrecnv  12961  gcdval  14005  imasvscafn  14792  imasvscaval  14793  grpsubval  15903  isghm  16072  lactghmga  16234  efgmval  16536  efgtval  16547  frgpup3lem  16601  dvrval  17135  psrvsca  17843  frlmval  18574  mat1comp  18737  mamulid  18738  mamurid  18739  madufval  18934  xkococnlem  19923  xkococn  19924  cnextval  20324  dscmet  20856  cncfval  21155  htpycom  21239  htpyid  21240  phtpycom  21251  phtpyid  21252  isismt  23677  grpodivval  24949  gxval  24964  ipval  25317  lnoval  25371  nmoofval  25381  bloval  25400  0ofval  25406  ajfval  25428  hvsubval  25637  hosmval  26358  hommval  26359  hodmval  26360  hfsmval  26361  hfmmval  26362  kbfval  26575  opsqrlem3  26765  xdivval  27311  fvproj  27526  pstmfval  27539  logbval  27676  sxval  27829  ismbfm  27891  dya2iocival  27912  sitgval  27942  sitmval  27958  oddpwdcv  27962  ballotlemgval  28130  cvmlift2lem4  28419  elgiso  28539  risefacval  28735  fallfacval  28736  metf1o  29879  heiborlem3  29940  heiborlem6  29943  heiborlem8  29945  heibor  29948  lcmval  30826  dpval  32263  ldualvs  33952  tendopl  35590  cdlemkuu  35709  dvavsca  35831  dvhvaddval  35905  dvhvscaval  35914  hlhilipval  36767
  Copyright terms: Public domain W3C validator