Theorem ovmpt2a 6446

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

Syntax hints:   -> wi 4   /\ wa 376   = wceq 1452   e. wcel 1904   _Vcvv 3031  (class class class)co 6308   |-> cmpt2 6310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-iota 5553  df-fun 5591  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313

This theorem is referenced by:  1st2val  6838  2nd2val  6839  cantnffval  8186  cantnfsuc  8193  fseqenlem1  8473  xaddval  11539  xmulval  11541  fzoval  11948  expval  12312  ccatfval  12770  splcl  12913  cshfn  12946  bpolylem  14178  ruclem1  14360  sadfval  14505  sadcp1  14508  smufval  14530  smupp1  14533  eucalgval2  14619  pcval  14873  pc0  14883  vdwapval  15002  pwsval  15462  xpsfval  15551  xpsval  15556  rescval  15810  isfunc  15847  isfull  15893  isfth  15897  natfval  15929  catcisolem  16079  xpchom  16143  1stfval  16154  2ndfval  16157  yonedalem3a  16237  yonedainv  16244  plusfval  16572  ismhm  16662  mulgval  16838  eqgfval  16943  isga  17023  subgga  17032  cayleylem1  17131  sylow1lem2  17329  isslw  17338  sylow2blem1  17350  sylow3lem1  17357  sylow3lem6  17362  frgpuptinv  17499  frgpup2  17504  isrhm  18027  scafval  18188  islmhm  18328  psrmulfval  18686  mplval  18729  ltbval  18772  mpfrcl  18818  evlsval  18819  evlval  18824  xrsdsval  19089  ipfval  19293  dsmmval  19374  matval  19513  submafval  19681  mdetfval  19688  minmar1fval  19748  txval  20656  xkoval  20679  hmeofval  20850  flffval  21082  qustgplem  21213  dscmet  21665  dscopn  21666  tngval  21725  nmofval  21797  nghmfval  21805  nmofvalOLD  21816  nghmfvalOLD  21823  isnmhm  21845  htpyco1  22087  htpycc  22089  phtpycc  22100  reparphti  22106  pcoval  22120  pcohtpylem  22128  pcorevlem  22135  dyadval  22629  itg1addlem3  22735  itg1addlem4  22736  mbfi1fseqlem3  22754  mbfi1fseqlem4  22755  mbfi1fseqlem5  22756  mbfi1fseqlem6  22757  mdegfval  23090  quotval  23324  elqaalem2  23352  elqaalem2OLD  23355  cxpval  23688  cxpcn3  23767  angval  23809  sgmval  24148  lgsval  24307  clwwlknprop  25579  rusgranumwlklem2  25757  numclwwlkovf  25888  numclwwlkovg  25894  numclwwlkovq  25906  numclwwlkovh  25908  shsval  27046  sshjval  27084  faeval  29142  txsconlem  30035  cvxscon  30038  iscvm  30054  cvmliftlem5  30084  rngohomval  32267  rngoisoval  32280  rmxfval  35823  rmyfval  35824  mendplusg  36123  mendvsca  36128  addrval  36889  subrval  36890  mulvval  36891  sigarval  38605  ismgmhm  40291  dmatALTval  40701