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

Theorem ovmpt2 6335
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 6334 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  S  e.  _V )  ->  ( A F B )  =  S )
61, 5mp3an3 1304 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   _Vcvv 3076  (class class class)co 6199    |-> cmpt2 6201
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-iota 5488  df-fun 5527  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204
This theorem is referenced by:  seqomlem1  7014  seqomlem4  7017  oav  7060  omv  7061  oev  7063  iunfictbso  8394  fin23lem12  8610  axdc4lem  8734  axcclem  8736  addpipq2  9215  mulpipq2  9218  subval  9711  divval  10106  cnref1o  11096  ixxval  11418  fzval  11555  modval  11826  om2uzrdg  11895  uzrdgsuci  11899  axdc4uzlem  11920  seqval  11933  seqp1  11937  bcval  12196  cnrecnv  12771  gcdval  13809  imasvscafn  14593  imasvscaval  14594  grpsubval  15699  isghm  15865  lactghmga  16027  efgmval  16329  efgtval  16340  frgpup3lem  16394  dvrval  16899  psrvsca  17584  frlmval  18297  dmatcomp  18427  mamulid  18428  mamurid  18429  madufval  18574  xkococnlem  19363  xkococn  19364  cnextval  19764  dscmet  20296  cncfval  20595  htpycom  20679  htpyid  20680  phtpycom  20691  phtpyid  20692  grpodivval  23881  gxval  23896  ipval  24249  lnoval  24303  nmoofval  24313  bloval  24332  0ofval  24338  ajfval  24360  hvsubval  24569  hosmval  25290  hommval  25291  hodmval  25292  hfsmval  25293  hfmmval  25294  kbfval  25507  opsqrlem3  25697  xdivval  26238  pstmfval  26467  logbval  26595  sxval  26748  ismbfm  26810  dya2iocival  26831  sitgval  26861  sitmval  26877  oddpwdcv  26881  ballotlemgval  27049  cvmlift2lem4  27338  elgiso  27458  risefacval  27654  fallfacval  27655  metf1o  28798  heiborlem3  28859  heiborlem6  28862  heiborlem8  28864  heibor  28867  dpval  31418  ldualvs  33105  tendopl  34743  cdlemkuu  34862  dvavsca  34984  dvhvaddval  35058  dvhvscaval  35067  hlhilipval  35920
  Copyright terms: Public domain W3C validator