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

Theorem ovmpt2a 5994
Description: Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
Hypotheses
Ref Expression
ovmpt2ga.1  |-  ( ( x  =  A  /\  y  =  B )  ->  R  =  S )
ovmpt2ga.2  |-  F  =  ( x  e.  C ,  y  e.  D  |->  R )
ovmpt2a.4  |-  S  e. 
_V
Assertion
Ref Expression
ovmpt2a  |-  ( ( 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)

Proof of Theorem ovmpt2a
StepHypRef Expression
1 ovmpt2a.4 . 2  |-  S  e. 
_V
2 ovmpt2ga.1 . . 3  |-  ( ( x  =  A  /\  y  =  B )  ->  R  =  S )
3 ovmpt2ga.2 . . 3  |-  F  =  ( x  e.  C ,  y  e.  D  |->  R )
42, 3ovmpt2ga 5993 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  S  e.  _V )  ->  ( A F B )  =  S )
51, 4mp3an3 1266 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A F B )  =  S )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696   _Vcvv 2801  (class class class)co 5874    e. cmpt2 5876
This theorem is referenced by:  1st2val  6161  2nd2val  6162  cantnffval  7380  cantnfsuc  7387  fseqenlem1  7667  xaddval  10566  xmulval  10568  fzoval  10892  expval  11122  ccatfval  11444  splcl  11483  ruclem1  12525  sadfval  12659  sadcp1  12662  smufval  12684  smupp1  12687  eucalgval2  12767  pcval  12913  pc0  12923  vdwapval  13036  pwsval  13401  xpsfval  13485  xpsval  13490  rescval  13720  isfunc  13754  isfull  13800  isfth  13804  natfval  13836  catcisolem  13954  xpchom  13970  1stfval  13981  2ndfval  13984  yonedalem3a  14064  yonedainv  14071  plusfval  14396  ismhm  14433  mulgval  14585  eqgfval  14681  isga  14761  subgga  14770  cayleylem1  14803  sylow1lem2  14926  isslw  14935  sylow2blem1  14947  sylow3lem1  14954  sylow3lem6  14959  frgpuptinv  15096  frgpup2  15101  isrhm  15517  scafval  15662  islmhm  15800  psrmulfval  16146  mplval  16189  ltbval  16229  xrsdsval  16431  ipfval  16569  txval  17275  xkoval  17298  hmeofval  17465  flffval  17700  divstgplem  17819  dscmet  18111  dscopn  18112  tngval  18171  nmofval  18239  nghmfval  18247  isnmhm  18271  htpyco1  18492  htpycc  18494  phtpycc  18505  reparphti  18511  pcoval  18525  pcohtpylem  18533  pcorevlem  18540  dyadval  18963  itg1addlem3  19069  itg1addlem4  19070  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  mpfrcl  19418  evlsval  19419  evlval  19424  mdegfval  19464  quotval  19688  elqaalem2  19716  cxpval  20027  cxpcn3  20104  angval  20115  sgmval  20396  lgsval  20555  shsval  21907  sshjval  21945  txsconlem  23786  cvxscon  23789  iscvm  23805  cvmliftlem5  23835  bpolylem  24855  ishomb  25891  isfuna  25937  propsrc  25971  rngohomval  26698  rngoisoval  26711  rmxfval  27092  rmyfval  27093  dsmmval  27303  matval  27568  mdetfval  27590  mendplusg  27597  mendvsca  27602  addrval  27774  subrval  27775  mulvval  27776  sigarval  27943
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879
  Copyright terms: Public domain W3C validator