Theorem ovmpt2a 6406

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 6405	. 2 |- ( ( A e. C /\ B e. D /\ S e. _V ) -> ( A F B ) = S )
5	1, 4	mp3an3 1311	1 |- ( ( A e. C /\ B e. D ) -> ( A F B ) = S )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   e. wcel 1823   _Vcvv 3106  (class class class)co 6270   |-> cmpt2 6272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-iota 5534  df-fun 5572  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275

This theorem is referenced by:  1st2val  6799  2nd2val  6800  cantnffval  8071  cantnfsuc  8080  cantnfsucOLD  8110  fseqenlem1  8396  xaddval  11425  xmulval  11427  fzoval  11805  expval  12150  ccatfval  12581  splcl  12719  cshfn  12752  ruclem1  14048  sadfval  14186  sadcp1  14189  smufval  14211  smupp1  14214  eucalgval2  14294  pcval  14452  pc0  14462  vdwapval  14575  pwsval  14975  xpsfval  15056  xpsval  15061  rescval  15315  isfunc  15352  isfull  15398  isfth  15402  natfval  15434  catcisolem  15584  xpchom  15648  1stfval  15659  2ndfval  15662  yonedalem3a  15742  yonedainv  15749  plusfval  16077  ismhm  16167  mulgval  16343  eqgfval  16448  isga  16528  subgga  16537  cayleylem1  16636  sylow1lem2  16818  isslw  16827  sylow2blem1  16839  sylow3lem1  16846  sylow3lem6  16851  frgpuptinv  16988  frgpup2  16993  isrhm  17565  scafval  17726  islmhm  17868  psrmulfval  18233  mplval  18279  ltbval  18331  mpfrcl  18382  evlsval  18383  evlval  18388  xrsdsval  18657  ipfval  18857  dsmmval  18938  matval  19080  submafval  19248  mdetfval  19255  minmar1fval  19315  txval  20231  xkoval  20254  hmeofval  20425  flffval  20656  qustgplem  20785  dscmet  21259  dscopn  21260  tngval  21319  nmofval  21387  nghmfval  21395  isnmhm  21419  htpyco1  21644  htpycc  21646  phtpycc  21657  reparphti  21663  pcoval  21677  pcohtpylem  21685  pcorevlem  21692  dyadval  22167  itg1addlem3  22271  itg1addlem4  22272  mbfi1fseqlem3  22290  mbfi1fseqlem4  22291  mbfi1fseqlem5  22292  mbfi1fseqlem6  22293  mdegfval  22626  quotval  22854  elqaalem2  22882  cxpval  23213  cxpcn3  23290  angval  23332  sgmval  23614  lgsval  23773  clwwlknprop  24974  rusgranumwlklem2  25152  numclwwlkovf  25283  numclwwlkovg  25289  numclwwlkovq  25301  numclwwlkovh  25303  shsval  26428  sshjval  26466  faeval  28455  txsconlem  28949  cvxscon  28952  iscvm  28968  cvmliftlem5  28998  bpolylem  30038  rngohomval  30607  rngoisoval  30620  rmxfval  31079  rmyfval  31080  mendplusg  31376  mendvsca  31381  addrval  31616  subrval  31617  mulvval  31618  sigarval  32306  ismgmhm  32843  dmatALTval  33255