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

Theorem ovmpt2 6337
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 6336 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  S  e.  _V )  ->  ( A F B )  =  S )
61, 5mp3an3 1311 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399    e. wcel 1826   _Vcvv 3034  (class class class)co 6196    |-> cmpt2 6198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-iota 5460  df-fun 5498  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201
This theorem is referenced by:  seqomlem1  7033  seqomlem4  7036  oav  7079  omv  7080  oev  7082  iunfictbso  8408  fin23lem12  8624  axdc4lem  8748  axcclem  8750  addpipq2  9225  mulpipq2  9228  subval  9724  divval  10126  cnref1o  11134  ixxval  11458  fzval  11595  modval  11898  om2uzrdg  11970  uzrdgsuci  11974  axdc4uzlem  11995  seqval  12021  seqp1  12025  bcval  12284  cnrecnv  13000  gcdval  14148  imasvscafn  14944  imasvscaval  14945  grpsubval  16210  isghm  16384  lactghmga  16546  efgmval  16847  efgtval  16858  frgpup3lem  16912  dvrval  17447  psrvsca  18157  frlmval  18870  mat1comp  19027  mamulid  19028  mamurid  19029  madufval  19224  xkococnlem  20245  xkococn  20246  cnextval  20646  dscmet  21178  cncfval  21477  htpycom  21561  htpyid  21562  phtpycom  21573  phtpyid  21574  logbval  23224  isismt  24041  grpodivval  25362  gxval  25377  ipval  25730  lnoval  25784  nmoofval  25794  bloval  25813  0ofval  25819  ajfval  25841  hvsubval  26050  hosmval  26770  hommval  26771  hodmval  26772  hfsmval  26773  hfmmval  26774  kbfval  26987  opsqrlem3  27177  xdivval  27768  fvproj  27989  pstmfval  28029  sxval  28317  ismbfm  28379  dya2iocival  28400  sitgval  28457  sitmval  28473  oddpwdcv  28477  ballotlemgval  28645  cvmlift2lem4  28940  elgiso  29225  risefacval  29296  fallfacval  29297  metf1o  30414  heiborlem3  30475  heiborlem6  30478  heiborlem8  30480  heibor  30483  lcmval  31366  dpval  33500  ldualvs  35275  tendopl  36915  cdlemkuu  37034  dvavsca  37156  dvhvaddval  37230  dvhvscaval  37239  hlhilipval  38092
  Copyright terms: Public domain W3C validator