Theorem ovmpt2a 6216

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   _Vcvv 2966  (class class class)co 6086   e. cmpt2 6088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pr 4524

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-iota 5374  df-fun 5413  df-fv 5419  df-ov 6089  df-oprab 6090  df-mpt2 6091

This theorem is referenced by:  1st2val  6597  2nd2val  6598  cantnffval  7861  cantnfsuc  7870  cantnfsucOLD  7900  fseqenlem1  8186  xaddval  11185  xmulval  11187  fzoval  11546  expval  11859  ccatfval  12265  splcl  12386  cshfn  12419  ruclem1  13505  sadfval  13640  sadcp1  13643  smufval  13665  smupp1  13668  eucalgval2  13748  pcval  13903  pc0  13913  vdwapval  14026  pwsval  14416  xpsfval  14497  xpsval  14502  rescval  14732  isfunc  14766  isfull  14812  isfth  14816  natfval  14848  catcisolem  14966  xpchom  14982  1stfval  14993  2ndfval  14996  yonedalem3a  15076  yonedainv  15083  plusfval  15420  ismhm  15458  mulgval  15618  eqgfval  15718  isga  15798  subgga  15807  cayleylem1  15906  sylow1lem2  16087  isslw  16096  sylow2blem1  16108  sylow3lem1  16115  sylow3lem6  16120  frgpuptinv  16257  frgpup2  16262  isrhm  16797  scafval  16943  islmhm  17082  psrmulfval  17430  mplval  17475  ltbval  17525  mpfrcl  17576  evlsval  17577  evlval  17582  xrsdsval  17826  ipfval  18047  dsmmval  18128  matval  18280  submafval  18359  mdetfval  18366  minmar1fval  18421  txval  19106  xkoval  19129  hmeofval  19300  flffval  19531  divstgplem  19660  dscmet  20134  dscopn  20135  tngval  20194  nmofval  20262  nghmfval  20270  isnmhm  20294  htpyco1  20519  htpycc  20521  phtpycc  20532  reparphti  20538  pcoval  20552  pcohtpylem  20560  pcorevlem  20567  dyadval  21041  itg1addlem3  21145  itg1addlem4  21146  mbfi1fseqlem3  21164  mbfi1fseqlem4  21165  mbfi1fseqlem5  21166  mbfi1fseqlem6  21167  mdegfval  21500  quotval  21727  elqaalem2  21755  cxpval  22078  cxpcn3  22155  angval  22166  sgmval  22449  lgsval  22608  shsval  24660  sshjval  24698  faeval  26610  txsconlem  27077  cvxscon  27080  iscvm  27096  cvmliftlem5  27126  bpolylem  28138  rngohomval  28713  rngoisoval  28726  rmxfval  29188  rmyfval  29189  mendplusg  29486  mendvsca  29491  addrval  29665  subrval  29666  mulvval  29667  sigarval  29829  rusgranumwlklem2  30511  numclwwlkovf  30617  numclwwlkovg  30623  numclwwlkovq  30635  numclwwlkovh  30637