Theorem ovmpoa 7563

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475  (class class class)co 7409   ∈ cmpo 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414

This theorem is referenced by:  1st2val  8003  2nd2val  8004  mptmpoopabbrd  8067  cantnffval  9658  cantnfsuc  9665  fseqenlem1  10019  xaddval  13202  xmulval  13204  fzoval  13633  expval  14029  ccatfval  14523  splcl  14702  cshfn  14740  bpolylem  15992  ruclem1  16174  sadfval  16393  sadcp1  16396  smufval  16418  smupp1  16421  eucalgval2  16518  pcval  16777  pc0  16787  vdwapval  16906  pwsval  17432  xpsfval  17512  xpsval  17516  rescval  17774  isfunc  17814  isfull  17861  isfth  17865  natfval  17897  catcisolem  18060  xpchom  18132  1stfval  18143  2ndfval  18146  yonedalem3a  18227  yonedainv  18234  plusfval  18568  ismhm  18673  mulgval  18954  eqgfval  19056  isga  19155  subgga  19164  cayleylem1  19280  sylow1lem2  19467  isslw  19476  sylow2blem1  19488  sylow3lem1  19495  sylow3lem6  19500  frgpuptinv  19639  frgpup2  19644  isrhm  20257  scafval  20491  islmhm  20638  xrsdsval  20989  ipfval  21202  dsmmval  21289  psrmulfval  21504  mplval  21548  ltbval  21598  mpfrcl  21648  evlsval  21649  evlval  21658  mhpfval  21682  matval  21911  submafval  22081  mdetfval  22088  minmar1fval  22148  txval  23068  xkoval  23091  hmeofval  23262  flffval  23493  qustgplem  23625  dscmet  24081  dscopn  24082  tngval  24148  nmofval  24231  nghmfval  24239  isnmhm  24263  htpyco1  24494  htpycc  24496  phtpycc  24507  reparphti  24513  pcoval  24527  pcohtpylem  24535  pcorevlem  24542  dyadval  25109  itg1addlem3  25215  itg1addlem4  25216  itg1addlem4OLD  25217  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  mdegfval  25580  quotval  25805  elqaalem2  25833  cxpval  26172  cxpcn3  26256  angval  26306  sgmval  26646  lgsval  26804  wwlksn  29091  wspthsn  29102  rusgrnumwwlklem  29224  clwwlkn  29279  2clwwlk  29600  numclwwlkovh0  29625  numclwwlkovq  29627  shsval  30565  sshjval  30603  faeval  33244  txsconnlem  34231  cvxsconn  34234  iscvm  34250  cvmliftlem5  34280  gg-reparphti  35172  rngohomval  36832  rngoisoval  36845  evlselv  41159  prjcrvfval  41373  rmxfval  41642  rmyfval  41643  mendplusg  41928  mendvsca  41933  mnringvald  42967  addrval  43225  subrval  43226  mulvval  43227  sigarval  45566  ismgmhm  46553  dmatALTval  47081  naryfval  47314