Theorem ovmpt2a 6791

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

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   _Vcvv 3200  (class class class)co 6650   |-> cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  1st2val  7194  2nd2val  7195  cantnffval  8560  cantnfsuc  8567  fseqenlem1  8847  xaddval  12054  xmulval  12056  fzoval  12471  expval  12862  ccatfval  13358  splcl  13503  cshfn  13536  bpolylem  14779  ruclem1  14960  sadfval  15174  sadcp1  15177  smufval  15199  smupp1  15202  eucalgval2  15294  pcval  15549  pc0  15559  vdwapval  15677  pwsval  16146  xpsfval  16227  xpsval  16232  rescval  16487  isfunc  16524  isfull  16570  isfth  16574  natfval  16606  catcisolem  16756  xpchom  16820  1stfval  16831  2ndfval  16834  yonedalem3a  16914  yonedainv  16921  plusfval  17248  ismhm  17337  mulgval  17543  eqgfval  17642  isga  17724  subgga  17733  cayleylem1  17832  sylow1lem2  18014  isslw  18023  sylow2blem1  18035  sylow3lem1  18042  sylow3lem6  18047  frgpuptinv  18184  frgpup2  18189  isrhm  18721  scafval  18882  islmhm  19027  psrmulfval  19385  mplval  19428  ltbval  19471  mpfrcl  19518  evlsval  19519  evlval  19524  xrsdsval  19790  ipfval  19994  dsmmval  20078  matval  20217  submafval  20385  mdetfval  20392  minmar1fval  20452  txval  21367  xkoval  21390  hmeofval  21561  flffval  21793  qustgplem  21924  dscmet  22377  dscopn  22378  tngval  22443  nmofval  22518  nghmfval  22526  isnmhm  22550  htpyco1  22777  htpycc  22779  phtpycc  22790  reparphti  22797  pcoval  22811  pcohtpylem  22819  pcorevlem  22826  dyadval  23360  itg1addlem3  23465  itg1addlem4  23466  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  mdegfval  23822  quotval  24047  elqaalem2  24075  cxpval  24410  cxpcn3  24489  angval  24531  sgmval  24868  lgsval  25026  wspthsn  26735  rusgrnumwwlklem  26865  numclwwlkovf  27213  numclwwlkovg  27220  numclwwlkovq  27232  numclwwlkovh  27234  shsval  28171  sshjval  28209  faeval  30309  txsconnlem  31222  cvxsconn  31225  iscvm  31241  cvmliftlem5  31271  rngohomval  33763  rngoisoval  33776  rmxfval  37468  rmyfval  37469  mendplusg  37756  mendvsca  37761  addrval  38670  subrval  38671  mulvval  38672  sigarval  41039  ismgmhm  41783  dmatALTval  42189