Theorem ovmpt2a 6418

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1383   e. wcel 1804   _Vcvv 3095  (class class class)co 6281   |-> cmpt2 6283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-iota 5541  df-fun 5580  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286

This theorem is referenced by:  1st2val  6811  2nd2val  6812  cantnffval  8083  cantnfsuc  8092  cantnfsucOLD  8122  fseqenlem1  8408  xaddval  11431  xmulval  11433  fzoval  11809  expval  12147  ccatfval  12571  splcl  12707  cshfn  12740  ruclem1  13841  sadfval  13979  sadcp1  13982  smufval  14004  smupp1  14007  eucalgval2  14087  pcval  14245  pc0  14255  vdwapval  14368  pwsval  14760  xpsfval  14841  xpsval  14846  rescval  15073  isfunc  15107  isfull  15153  isfth  15157  natfval  15189  catcisolem  15307  xpchom  15323  1stfval  15334  2ndfval  15337  yonedalem3a  15417  yonedainv  15424  plusfval  15752  ismhm  15842  mulgval  16018  eqgfval  16123  isga  16203  subgga  16212  cayleylem1  16311  sylow1lem2  16493  isslw  16502  sylow2blem1  16514  sylow3lem1  16521  sylow3lem6  16526  frgpuptinv  16663  frgpup2  16668  isrhm  17244  scafval  17405  islmhm  17547  psrmulfval  17912  mplval  17958  ltbval  18010  mpfrcl  18061  evlsval  18062  evlval  18067  xrsdsval  18336  ipfval  18557  dsmmval  18638  matval  18786  submafval  18954  mdetfval  18961  minmar1fval  19021  txval  19938  xkoval  19961  hmeofval  20132  flffval  20363  qustgplem  20492  dscmet  20966  dscopn  20967  tngval  21026  nmofval  21094  nghmfval  21102  isnmhm  21126  htpyco1  21351  htpycc  21353  phtpycc  21364  reparphti  21370  pcoval  21384  pcohtpylem  21392  pcorevlem  21399  dyadval  21874  itg1addlem3  21978  itg1addlem4  21979  mbfi1fseqlem3  21997  mbfi1fseqlem4  21998  mbfi1fseqlem5  21999  mbfi1fseqlem6  22000  mdegfval  22333  quotval  22560  elqaalem2  22588  cxpval  22917  cxpcn3  22994  angval  23005  sgmval  23288  lgsval  23447  clwwlknprop  24644  rusgranumwlklem2  24822  numclwwlkovf  24953  numclwwlkovg  24959  numclwwlkovq  24971  numclwwlkovh  24973  shsval  26102  sshjval  26140  faeval  28091  txsconlem  28558  cvxscon  28561  iscvm  28577  cvmliftlem5  28607  bpolylem  29785  rngohomval  30342  rngoisoval  30355  rmxfval  30815  rmyfval  30816  mendplusg  31111  mendvsca  31116  addrval  31329  subrval  31330  mulvval  31331  sigarval  31905  ismgmhm  32309  dmatALTval  32731