Theorem ovmpoa 7406

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 7405	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
5	1, 4	mp3an3 1448	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422  (class class class)co 7255   ∈ cmpo 7257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260

This theorem is referenced by:  1st2val  7832  2nd2val  7833  cantnffval  9351  cantnfsuc  9358  fseqenlem1  9711  xaddval  12886  xmulval  12888  fzoval  13317  expval  13712  ccatfval  14204  splcl  14393  cshfn  14431  bpolylem  15686  ruclem1  15868  sadfval  16087  sadcp1  16090  smufval  16112  smupp1  16115  eucalgval2  16214  pcval  16473  pc0  16483  vdwapval  16602  pwsval  17114  xpsfval  17194  xpsval  17198  rescval  17456  isfunc  17495  isfull  17542  isfth  17546  natfval  17578  catcisolem  17741  xpchom  17813  1stfval  17824  2ndfval  17827  yonedalem3a  17908  yonedainv  17915  plusfval  18248  ismhm  18347  mulgval  18619  eqgfval  18719  isga  18812  subgga  18821  cayleylem1  18935  sylow1lem2  19119  isslw  19128  sylow2blem1  19140  sylow3lem1  19147  sylow3lem6  19152  frgpuptinv  19292  frgpup2  19297  isrhm  19880  scafval  20057  islmhm  20204  xrsdsval  20554  ipfval  20766  dsmmval  20851  psrmulfval  21064  mplval  21107  ltbval  21154  mpfrcl  21205  evlsval  21206  evlval  21215  mhpfval  21239  matval  21468  submafval  21636  mdetfval  21643  minmar1fval  21703  txval  22623  xkoval  22646  hmeofval  22817  flffval  23048  qustgplem  23180  dscmet  23634  dscopn  23635  tngval  23701  nmofval  23784  nghmfval  23792  isnmhm  23816  htpyco1  24047  htpycc  24049  phtpycc  24060  reparphti  24066  pcoval  24080  pcohtpylem  24088  pcorevlem  24095  dyadval  24661  itg1addlem3  24767  itg1addlem4  24768  itg1addlem4OLD  24769  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  mdegfval  25132  quotval  25357  elqaalem2  25385  cxpval  25724  cxpcn3  25806  angval  25856  sgmval  26196  lgsval  26354  wwlksn  28103  wspthsn  28114  rusgrnumwwlklem  28236  clwwlkn  28291  2clwwlk  28612  numclwwlkovh0  28637  numclwwlkovq  28639  shsval  29575  sshjval  29613  faeval  32114  txsconnlem  33102  cvxsconn  33105  iscvm  33121  cvmliftlem5  33151  rngohomval  36049  rngoisoval  36062  rmxfval  40642  rmyfval  40643  mendplusg  40927  mendvsca  40932  mnringvald  41715  addrval  41973  subrval  41974  mulvval  41975  sigarval  44253  ismgmhm  45225  dmatALTval  45629  naryfval  45862