Theorem ovmpt2a 6408

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1374   e. wcel 1762   _Vcvv 3106  (class class class)co 6275   |-> cmpt2 6277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-iota 5542  df-fun 5581  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280

This theorem is referenced by:  1st2val  6800  2nd2val  6801  cantnffval  8069  cantnfsuc  8078  cantnfsucOLD  8108  fseqenlem1  8394  xaddval  11411  xmulval  11413  fzoval  11787  expval  12124  ccatfval  12544  splcl  12678  cshfn  12711  ruclem1  13814  sadfval  13950  sadcp1  13953  smufval  13975  smupp1  13978  eucalgval2  14058  pcval  14216  pc0  14226  vdwapval  14339  pwsval  14730  xpsfval  14811  xpsval  14816  rescval  15046  isfunc  15080  isfull  15126  isfth  15130  natfval  15162  catcisolem  15280  xpchom  15296  1stfval  15307  2ndfval  15310  yonedalem3a  15390  yonedainv  15397  plusfval  15734  ismhm  15772  mulgval  15937  eqgfval  16037  isga  16117  subgga  16126  cayleylem1  16225  sylow1lem2  16408  isslw  16417  sylow2blem1  16429  sylow3lem1  16436  sylow3lem6  16441  frgpuptinv  16578  frgpup2  16583  isrhm  17147  scafval  17307  islmhm  17449  psrmulfval  17802  mplval  17848  ltbval  17900  mpfrcl  17951  evlsval  17952  evlval  17957  xrsdsval  18223  ipfval  18444  dsmmval  18525  matval  18673  submafval  18841  mdetfval  18848  minmar1fval  18908  txval  19793  xkoval  19816  hmeofval  19987  flffval  20218  divstgplem  20347  dscmet  20821  dscopn  20822  tngval  20881  nmofval  20949  nghmfval  20957  isnmhm  20981  htpyco1  21206  htpycc  21208  phtpycc  21219  reparphti  21225  pcoval  21239  pcohtpylem  21247  pcorevlem  21254  dyadval  21729  itg1addlem3  21833  itg1addlem4  21834  mbfi1fseqlem3  21852  mbfi1fseqlem4  21853  mbfi1fseqlem5  21854  mbfi1fseqlem6  21855  mdegfval  22188  quotval  22415  elqaalem2  22443  cxpval  22766  cxpcn3  22843  angval  22854  sgmval  23137  lgsval  23296  rusgranumwlklem2  24612  numclwwlkovf  24744  numclwwlkovg  24750  numclwwlkovq  24762  numclwwlkovh  24764  shsval  25892  sshjval  25930  faeval  27844  txsconlem  28311  cvxscon  28314  iscvm  28330  cvmliftlem5  28360  bpolylem  29373  rngohomval  29957  rngoisoval  29970  rmxfval  30431  rmyfval  30432  mendplusg  30729  mendvsca  30734  addrval  30908  subrval  30909  mulvval  30910  sigarval  31489  dmatALTval  31949