Theorem ovmpt2a 6689

Description: Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)

Hypotheses

Ref	Expression
ovmpt2ga.1	⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
ovmpt2ga.2	⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
ovmpt2a.4	⊢ 𝑆 ∈ V

Assertion

Ref	Expression
ovmpt2a	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦

Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem ovmpt2a

Step	Hyp	Ref	Expression
1		ovmpt2a.4	. 2 ⊢ 𝑆 ∈ V
2		ovmpt2ga.1	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
3		ovmpt2ga.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
4	2, 3	ovmpt2ga 6688	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
5	1, 4	mp3an3 1405	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Vcvv 3173  (class class class)co 6549   ↦ cmpt2 6551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554

This theorem is referenced by:  1st2val  7085  2nd2val  7086  cantnffval  8443  cantnfsuc  8450  fseqenlem1  8730  xaddval  11928  xmulval  11930  fzoval  12340  expval  12724  ccatfval  13211  splcl  13354  cshfn  13387  bpolylem  14618  ruclem1  14799  sadfval  15012  sadcp1  15015  smufval  15037  smupp1  15040  eucalgval2  15132  pcval  15387  pc0  15397  vdwapval  15515  pwsval  15969  xpsfval  16050  xpsval  16055  rescval  16310  isfunc  16347  isfull  16393  isfth  16397  natfval  16429  catcisolem  16579  xpchom  16643  1stfval  16654  2ndfval  16657  yonedalem3a  16737  yonedainv  16744  plusfval  17071  ismhm  17160  mulgval  17366  eqgfval  17465  isga  17547  subgga  17556  cayleylem1  17655  sylow1lem2  17837  isslw  17846  sylow2blem1  17858  sylow3lem1  17865  sylow3lem6  17870  frgpuptinv  18007  frgpup2  18012  isrhm  18544  scafval  18705  islmhm  18848  psrmulfval  19206  mplval  19249  ltbval  19292  mpfrcl  19339  evlsval  19340  evlval  19345  xrsdsval  19609  ipfval  19813  dsmmval  19897  matval  20036  submafval  20204  mdetfval  20211  minmar1fval  20271  txval  21177  xkoval  21200  hmeofval  21371  flffval  21603  qustgplem  21734  dscmet  22187  dscopn  22188  tngval  22253  nmofval  22328  nghmfval  22336  isnmhm  22360  htpyco1  22585  htpycc  22587  phtpycc  22598  reparphti  22605  pcoval  22619  pcohtpylem  22627  pcorevlem  22634  dyadval  23166  itg1addlem3  23271  itg1addlem4  23272  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  mdegfval  23626  quotval  23851  elqaalem2  23879  cxpval  24210  cxpcn3  24289  angval  24331  sgmval  24668  lgsval  24826  clwwlknprop  26300  rusgranumwlklem2  26477  numclwwlkovf  26608  numclwwlkovg  26614  numclwwlkovq  26626  numclwwlkovh  26628  shsval  27555  sshjval  27593  faeval  29636  txsconlem  30476  cvxscon  30479  iscvm  30495  cvmliftlem5  30525  rngohomval  32933  rngoisoval  32946  rmxfval  36486  rmyfval  36487  mendplusg  36775  mendvsca  36780  addrval  37691  subrval  37692  mulvval  37693  sigarval  39688  wspthsn  41046  rusgrnumwwlklem  41173  av-numclwwlkovf  41511  av-numclwwlkovg  41518  av-numclwwlkovq  41529  av-numclwwlkovh  41531  ismgmhm  41573  dmatALTval  41983