Theorem ovmpt2a 6224

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 6223	. 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 2975  (class class class)co 6094   e. cmpt2 6096

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 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534

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 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-iota 5384  df-fun 5423  df-fv 5429  df-ov 6097  df-oprab 6098  df-mpt2 6099

This theorem is referenced by:  1st2val  6605  2nd2val  6606  cantnffval  7872  cantnfsuc  7881  cantnfsucOLD  7911  fseqenlem1  8197  xaddval  11196  xmulval  11198  fzoval  11557  expval  11870  ccatfval  12276  splcl  12397  cshfn  12430  ruclem1  13516  sadfval  13651  sadcp1  13654  smufval  13676  smupp1  13679  eucalgval2  13759  pcval  13914  pc0  13924  vdwapval  14037  pwsval  14427  xpsfval  14508  xpsval  14513  rescval  14743  isfunc  14777  isfull  14823  isfth  14827  natfval  14859  catcisolem  14977  xpchom  14993  1stfval  15004  2ndfval  15007  yonedalem3a  15087  yonedainv  15094  plusfval  15431  ismhm  15469  mulgval  15632  eqgfval  15732  isga  15812  subgga  15821  cayleylem1  15920  sylow1lem2  16101  isslw  16110  sylow2blem1  16122  sylow3lem1  16129  sylow3lem6  16134  frgpuptinv  16271  frgpup2  16276  isrhm  16814  scafval  16970  islmhm  17111  psrmulfval  17459  mplval  17504  ltbval  17556  mpfrcl  17607  evlsval  17608  evlval  17613  xrsdsval  17860  ipfval  18081  dsmmval  18162  matval  18314  submafval  18393  mdetfval  18400  minmar1fval  18455  txval  19140  xkoval  19163  hmeofval  19334  flffval  19565  divstgplem  19694  dscmet  20168  dscopn  20169  tngval  20228  nmofval  20296  nghmfval  20304  isnmhm  20328  htpyco1  20553  htpycc  20555  phtpycc  20566  reparphti  20572  pcoval  20586  pcohtpylem  20594  pcorevlem  20601  dyadval  21075  itg1addlem3  21179  itg1addlem4  21180  mbfi1fseqlem3  21198  mbfi1fseqlem4  21199  mbfi1fseqlem5  21200  mbfi1fseqlem6  21201  mdegfval  21534  quotval  21761  elqaalem2  21789  cxpval  22112  cxpcn3  22189  angval  22200  sgmval  22483  lgsval  22642  shsval  24718  sshjval  24756  faeval  26665  txsconlem  27132  cvxscon  27135  iscvm  27151  cvmliftlem5  27181  bpolylem  28194  rngohomval  28773  rngoisoval  28786  rmxfval  29248  rmyfval  29249  mendplusg  29546  mendvsca  29551  addrval  29725  subrval  29726  mulvval  29727  sigarval  29889  rusgranumwlklem2  30571  numclwwlkovf  30677  numclwwlkovg  30683  numclwwlkovq  30695  numclwwlkovh  30697