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

Theorem ovmpt2a 5978
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 5977 . 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 1623    e. wcel 1684   _Vcvv 2788  (class class class)co 5858    e. cmpt2 5860
This theorem is referenced by:  1st2val  6145  2nd2val  6146  cantnffval  7364  cantnfsuc  7371  fseqenlem1  7651  xaddval  10550  xmulval  10552  fzoval  10876  expval  11106  ccatfval  11428  splcl  11467  ruclem1  12509  sadfval  12643  sadcp1  12646  smufval  12668  smupp1  12671  eucalgval2  12751  pcval  12897  pc0  12907  vdwapval  13020  pwsval  13385  xpsfval  13469  xpsval  13474  rescval  13704  isfunc  13738  isfull  13784  isfth  13788  natfval  13820  catcisolem  13938  xpchom  13954  1stfval  13965  2ndfval  13968  yonedalem3a  14048  yonedainv  14055  plusfval  14380  ismhm  14417  mulgval  14569  eqgfval  14665  isga  14745  subgga  14754  cayleylem1  14787  sylow1lem2  14910  isslw  14919  sylow2blem1  14931  sylow3lem1  14938  sylow3lem6  14943  frgpuptinv  15080  frgpup2  15085  isrhm  15501  scafval  15646  islmhm  15784  psrmulfval  16130  mplval  16173  ltbval  16213  xrsdsval  16415  ipfval  16553  txval  17259  xkoval  17282  hmeofval  17449  flffval  17684  divstgplem  17803  dscmet  18095  dscopn  18096  tngval  18155  nmofval  18223  nghmfval  18231  isnmhm  18255  htpyco1  18476  htpycc  18478  phtpycc  18489  reparphti  18495  pcoval  18509  pcohtpylem  18517  pcorevlem  18524  dyadval  18947  itg1addlem3  19053  itg1addlem4  19054  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  mpfrcl  19402  evlsval  19403  evlval  19408  mdegfval  19448  quotval  19672  elqaalem2  19700  cxpval  20011  cxpcn3  20088  angval  20099  sgmval  20380  lgsval  20539  shsval  21891  sshjval  21929  txsconlem  23771  cvxscon  23774  iscvm  23790  cvmliftlem5  23820  bpolylem  24783  ishomb  25788  isfuna  25834  propsrc  25868  rngohomval  26595  rngoisoval  26608  rmxfval  26989  rmyfval  26990  dsmmval  27200  matval  27465  mdetfval  27487  mendplusg  27494  mendvsca  27499  addrval  27671  subrval  27672  mulvval  27673  sigarval  27840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863
  Copyright terms: Public domain W3C validator