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

Theorem ovmpt2 6451
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 6450 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  S  e.  _V )  ->  ( A F B )  =  S )
61, 5mp3an3 1379 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    = wceq 1452    e. wcel 1904   _Vcvv 3031  (class class class)co 6308    |-> cmpt2 6310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-iota 5553  df-fun 5591  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313
This theorem is referenced by:  seqomlem1  7185  seqomlem4  7188  oav  7231  omv  7232  oev  7234  iunfictbso  8563  fin23lem12  8779  axdc4lem  8903  axcclem  8905  addpipq2  9379  mulpipq2  9382  subval  9886  divval  10294  cnref1o  11320  ixxval  11668  fzval  11812  modval  12131  om2uzrdg  12208  uzrdgsuci  12212  axdc4uzlem  12233  seqval  12262  seqp1  12266  bcval  12527  cnrecnv  13305  risefacval  14138  fallfacval  14139  gcdval  14549  lcmval  14634  lcmvalOLD  14635  imasvscafn  15521  imasvscaval  15522  grpsubval  16787  isghm  16961  lactghmga  17123  efgmval  17440  efgtval  17451  frgpup3lem  17505  dvrval  17991  psrvsca  18692  frlmval  19388  mat1comp  19542  mamulid  19543  mamurid  19544  madufval  19739  xkococnlem  20751  xkococn  20752  cnextval  21154  dscmet  21665  cncfval  21998  htpycom  22085  htpyid  22086  phtpycom  22097  phtpyid  22098  logbval  23782  isismt  24658  grpodivval  26052  gxval  26067  ipval  26420  lnoval  26474  nmoofval  26484  bloval  26503  0ofval  26509  ajfval  26531  hvsubval  26750  hosmval  27469  hommval  27470  hodmval  27471  hfsmval  27472  hfmmval  27473  kbfval  27686  opsqrlem3  27876  xdivval  28463  smatrcl  28696  smatlem  28697  mdetpmtr12  28725  fvproj  28733  pstmfval  28773  sxval  29086  ismbfm  29147  dya2iocival  29168  sitgval  29238  sitmval  29255  oddpwdcv  29261  ballotlemgval  29429  ballotlemgvalOLD  29467  cvmlift2lem4  30101  elgiso  30386  icoreval  31826  metf1o  32148  heiborlem3  32209  heiborlem6  32212  heiborlem8  32214  heibor  32217  ldualvs  32774  tendopl  34414  cdlemkuu  34533  dvavsca  34655  dvhvaddval  34729  dvhvscaval  34738  hlhilipval  35591  dpval  40997
  Copyright terms: Public domain W3C validator