Theorem ovmpt2a 6427

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

Step	Hyp	Ref	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 )
4	2, 3	ovmpt2ga 6426	. 2 |- ( ( A e. C /\ B e. D /\ S e. _V ) -> ( A F B ) = S )
5	1, 4	mp3an3 1353	1 |- ( ( A e. C /\ B e. D ) -> ( A F B ) = S )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1444   e. wcel 1887   _Vcvv 3045  (class class class)co 6290   |-> cmpt2 6292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-iota 5546  df-fun 5584  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295

This theorem is referenced by:  1st2val  6819  2nd2val  6820  cantnffval  8168  cantnfsuc  8175  fseqenlem1  8455  xaddval  11516  xmulval  11518  fzoval  11921  expval  12274  ccatfval  12719  splcl  12859  cshfn  12892  bpolylem  14101  ruclem1  14283  sadfval  14426  sadcp1  14429  smufval  14451  smupp1  14454  eucalgval2  14540  pcval  14794  pc0  14804  vdwapval  14923  pwsval  15384  xpsfval  15473  xpsval  15478  rescval  15732  isfunc  15769  isfull  15815  isfth  15819  natfval  15851  catcisolem  16001  xpchom  16065  1stfval  16076  2ndfval  16079  yonedalem3a  16159  yonedainv  16166  plusfval  16494  ismhm  16584  mulgval  16760  eqgfval  16865  isga  16945  subgga  16954  cayleylem1  17053  sylow1lem2  17251  isslw  17260  sylow2blem1  17272  sylow3lem1  17279  sylow3lem6  17284  frgpuptinv  17421  frgpup2  17426  isrhm  17949  scafval  18110  islmhm  18250  psrmulfval  18609  mplval  18652  ltbval  18695  mpfrcl  18741  evlsval  18742  evlval  18747  xrsdsval  19012  ipfval  19216  dsmmval  19297  matval  19436  submafval  19604  mdetfval  19611  minmar1fval  19671  txval  20579  xkoval  20602  hmeofval  20773  flffval  21004  qustgplem  21135  dscmet  21587  dscopn  21588  tngval  21647  nmofval  21719  nghmfval  21727  nmofvalOLD  21738  nghmfvalOLD  21745  isnmhm  21767  htpyco1  22009  htpycc  22011  phtpycc  22022  reparphti  22028  pcoval  22042  pcohtpylem  22050  pcorevlem  22057  dyadval  22550  itg1addlem3  22656  itg1addlem4  22657  mbfi1fseqlem3  22675  mbfi1fseqlem4  22676  mbfi1fseqlem5  22677  mbfi1fseqlem6  22678  mdegfval  23011  quotval  23245  elqaalem2  23273  elqaalem2OLD  23276  cxpval  23609  cxpcn3  23688  angval  23730  sgmval  24069  lgsval  24228  clwwlknprop  25500  rusgranumwlklem2  25678  numclwwlkovf  25809  numclwwlkovg  25815  numclwwlkovq  25827  numclwwlkovh  25829  shsval  26965  sshjval  27003  faeval  29069  txsconlem  29963  cvxscon  29966  iscvm  29982  cvmliftlem5  30012  rngohomval  32203  rngoisoval  32216  rmxfval  35752  rmyfval  35753  mendplusg  36052  mendvsca  36057  addrval  36819  subrval  36820  mulvval  36821  sigarval  38459  ismgmhm  39836  dmatALTval  40246