Theorem ovmpoa 7567

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem ovmpoa

Step	Hyp	Ref	Expression
1		ovmpoa.4	. 2 ⊢ 𝑆 ∈ V
2		ovmpoga.1	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
3		ovmpoga.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
4	2, 3	ovmpoga 7566	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
5	1, 4	mp3an3 1479	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3451  (class class class)co 7412   ∈ cmpo 7414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417

This theorem is used by:  ovmpot  7573  1st2val  8018  2nd2val  8019  mptmpoopabbrd  8083  cantnffval  9648  cantnfsuc  9655  fseqenlem1  10084  xaddval  13334  xmulval  13336  fzoval  13774  expval  14186  ccatfval  14698  splcl  14881  cshfn  14921  bpolylem  16194  ruclem1  16379  sadfval  16602  sadcp1  16605  smufval  16627  smupp1  16630  eucalgval2  16736  pcval  17002  pc0  17012  vdwapval  17131  pwsval  17637  xpsfval  17718  xpsval  17722  rescval  17982  isfunc  18019  isfull  18067  isfth  18071  natfval  18104  catcisolem  18265  xpchom  18334  1stfval  18345  2ndfval  18348  yonedalem3a  18428  yonedainv  18435  plusfval  18803  ismgmhm  18865  ismhm  18960  mulgval  19261  eqgfval  19368  isghm  19410  isga  19485  subgga  19494  cayleylem1  19606  sylow1lem2  19793  isslw  19802  sylow2blem1  19814  sylow3lem1  19821  sylow3lem6  19826  frgpuptinv  19965  frgpup2  19970  rhmval0  20685  isrhm  20689  scafval  21136  islmhm  21282  xrsdsval  21697  ipfval  21935  dsmmval  22020  psrmulfval  22231  mplval  22276  ltbval  22332  mpfrcl  22374  evlsval  22375  evlval  22389  mhpfval  22439  matval  22706  submafval  22874  mdetfval  22881  minmar1fval  22941  txval  23863  xkoval  23886  hmeofval  24057  flffval  24288  qustgplem  24420  dscmet  24871  dscopn  24872  tngval  24938  nmofval  25013  nghmfval  25021  isnmhm  25045  htpyco1  25279  htpycc  25281  phtpycc  25292  reparphti  25298  pcoval  25312  pcohtpylem  25320  pcorevlem  25327  dyadval  25893  itg1addlem3  25999  itg1addlem4  26000  mbfi1fseqlem3  26018  mbfi1fseqlem4  26019  mbfi1fseqlem5  26020  mbfi1fseqlem6  26021  mdegfval  26360  quotval  26595  elqaalem2  26625  cxpval  26974  cxpcn3  27058  angval  27111  sgmval  27451  lgsval  27610  wwlksn  30408  wspthsn  30419  rusgrnumwwlklem  30544  clwwlkn  30599  2clwwlk  30930  numclwwlkovh0  30955  numclwwlkovq  30957  shsval  31896  sshjval  31934  faeval  34861  txsconnlem  35974  cvxsconn  35977  iscvm  35993  cvmliftlem5  36023  mpomulnzcnf  37058  rngohomval  38866  rngoisoval  38879  evlselv  43579  prjcrvfval  43621  rmxfval  43864  rmyfval  43865  mendplusg  44142  mendvsca  44147  mnringvald  45170  addrval  45407  subrval  45408  mulvval  45409  sigarval  47804  dmatALTval  49456  naryfval  49684  discsubc  50116  oppfvalg  50178  upfval  50228  setc1onsubc  50654  lmdfval  50701  cmdfval  50702