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

Theorem ovmpt2 6221
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 6220 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  S  e.  _V )  ->  ( A F B )  =  S )
61, 5mp3an3 1303 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   _Vcvv 2967  (class class class)co 6086    e. cmpt2 6088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091
This theorem is referenced by:  seqomlem1  6897  seqomlem4  6900  oav  6943  omv  6944  oev  6946  iunfictbso  8276  fin23lem12  8492  axdc4lem  8616  axcclem  8618  addpipq2  9097  mulpipq2  9100  subval  9593  divval  9988  cnref1o  10978  ixxval  11300  fzval  11431  modval  11702  om2uzrdg  11771  uzrdgsuci  11775  axdc4uzlem  11796  seqval  11809  seqp1  11813  bcval  12072  cnrecnv  12646  gcdval  13684  imasvscafn  14467  imasvscaval  14468  grpsubval  15572  isghm  15738  lactghmga  15900  efgmval  16200  efgtval  16211  frgpup3lem  16265  dvrval  16765  psrvsca  17439  frlmval  18148  dmatcomp  18278  mamulid  18279  mamurid  18280  madufval  18418  xkococnlem  19207  xkococn  19208  cnextval  19608  dscmet  20140  cncfval  20439  htpycom  20523  htpyid  20524  phtpycom  20535  phtpyid  20536  grpodivval  23681  gxval  23696  ipval  24049  lnoval  24103  nmoofval  24113  bloval  24132  0ofval  24138  ajfval  24160  hvsubval  24369  hosmval  25090  hommval  25091  hodmval  25092  hfsmval  25093  hfmmval  25094  kbfval  25307  opsqrlem3  25497  xdivval  26045  pstmfval  26275  logbval  26403  sxval  26556  ismbfm  26619  dya2iocival  26640  sitgval  26670  sitmval  26686  oddpwdcv  26690  ballotlemgval  26858  cvmlift2lem4  27147  elgiso  27266  risefacval  27462  fallfacval  27463  metf1o  28604  heiborlem3  28665  heiborlem6  28668  heiborlem8  28670  heibor  28673  dpval  30994  ldualvs  32622  tendopl  34260  cdlemkuu  34379  dvavsca  34501  dvhvaddval  34575  dvhvscaval  34584  hlhilipval  35437
  Copyright terms: Public domain W3C validator