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

Theorem ovmpt2 6442
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 6441 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  S  e.  _V )  ->  ( A F B )  =  S )
61, 5mp3an3 1349 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1868   _Vcvv 3081  (class class class)co 6301    |-> cmpt2 6303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-iota 5561  df-fun 5599  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306
This theorem is referenced by:  seqomlem1  7171  seqomlem4  7174  oav  7217  omv  7218  oev  7220  iunfictbso  8545  fin23lem12  8761  axdc4lem  8885  axcclem  8887  addpipq2  9361  mulpipq2  9364  subval  9866  divval  10272  cnref1o  11297  ixxval  11643  fzval  11786  modval  12097  om2uzrdg  12169  uzrdgsuci  12173  axdc4uzlem  12194  seqval  12223  seqp1  12227  bcval  12488  cnrecnv  13216  risefacval  14048  fallfacval  14049  gcdval  14457  lcmval  14542  lcmvalOLD  14543  imasvscafn  15430  imasvscaval  15431  grpsubval  16696  isghm  16870  lactghmga  17032  efgmval  17349  efgtval  17360  frgpup3lem  17414  dvrval  17900  psrvsca  18602  frlmval  19297  mat1comp  19451  mamulid  19452  mamurid  19453  madufval  19648  xkococnlem  20660  xkococn  20661  cnextval  21062  dscmet  21573  cncfval  21906  htpycom  21993  htpyid  21994  phtpycom  22005  phtpyid  22006  logbval  23689  isismt  24565  grpodivval  25956  gxval  25971  ipval  26324  lnoval  26378  nmoofval  26388  bloval  26407  0ofval  26413  ajfval  26435  hvsubval  26654  hosmval  27373  hommval  27374  hodmval  27375  hfsmval  27376  hfmmval  27377  kbfval  27590  opsqrlem3  27780  xdivval  28382  smatrcl  28617  smatlem  28618  mdetpmtr12  28646  fvproj  28654  pstmfval  28694  sxval  29007  ismbfm  29069  dya2iocival  29090  sitgval  29160  sitmval  29177  oddpwdcv  29183  ballotlemgval  29351  ballotlemgvalOLD  29389  cvmlift2lem4  30024  elgiso  30309  icoreval  31696  metf1o  31997  heiborlem3  32058  heiborlem6  32061  heiborlem8  32063  heibor  32066  ldualvs  32621  tendopl  34261  cdlemkuu  34380  dvavsca  34502  dvhvaddval  34576  dvhvscaval  34585  hlhilipval  35438  dpval  39763
  Copyright terms: Public domain W3C validator