Theorem ovmpoa 7602

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454  (class class class)co 7446   ∈ cmpo 7448

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-iota 6515  df-fun 6563  df-fv 6569  df-ov 7449  df-oprab 7450  df-mpo 7451

This theorem is used by:  ovmpot  7608  1st2val  8056  2nd2val  8057  mptmpoopabbrd  8122  cantnffval  9694  cantnfsuc  9701  fseqenlem1  10133  xaddval  13383  xmulval  13385  fzoval  13824  expval  14236  ccatfval  14748  splcl  14932  cshfn  14972  bpolylem  16246  ruclem1  16431  sadfval  16654  sadcp1  16657  smufval  16679  smupp1  16682  eucalgval2  16788  pcval  17054  pc0  17064  vdwapval  17183  pwsval  17689  xpsfval  17770  xpsval  17774  rescval  18034  isfunc  18071  isfull  18119  isfth  18123  natfval  18156  catcisolem  18317  xpchom  18386  1stfval  18397  2ndfval  18400  yonedalem3a  18480  yonedainv  18487  plusfval  18855  ismgmhm  18917  ismhm  19012  mulgval  19313  eqgfval  19420  isghm  19462  isga  19538  subgga  19547  cayleylem1  19659  sylow1lem2  19846  isslw  19855  sylow2blem1  19867  sylow3lem1  19874  sylow3lem6  19879  frgpuptinv  20018  frgpup2  20023  rhmval0  20738  isrhm  20742  scafval  21189  islmhm  21335  xrsdsval  21750  ipfval  21988  dsmmval  22073  psrmulfval  22284  mplval  22329  ltbval  22385  mpfrcl  22427  evlsval  22428  evlval  22442  mhpfval  22492  matval  22759  submafval  22927  mdetfval  22934  minmar1fval  22994  txval  23916  xkoval  23939  hmeofval  24110  flffval  24341  qustgplem  24473  dscmet  24924  dscopn  24925  tngval  24991  nmofval  25066  nghmfval  25074  isnmhm  25098  htpyco1  25332  htpycc  25334  phtpycc  25345  reparphti  25351  pcoval  25365  pcohtpylem  25373  pcorevlem  25380  dyadval  25946  itg1addlem3  26052  itg1addlem4  26053  mbfi1fseqlem3  26071  mbfi1fseqlem4  26072  mbfi1fseqlem5  26073  mbfi1fseqlem6  26074  mdegfval  26413  quotval  26646  elqaalem2  26676  cxpval  27025  cxpcn3  27109  angval  27162  sgmval  27502  lgsval  27661  wwlksn  30459  wspthsn  30470  rusgrnumwwlklem  30595  clwwlkn  30650  2clwwlk  30981  numclwwlkovh0  31006  numclwwlkovq  31008  shsval  31947  sshjval  31985  faeval  34962  txsconnlem  36185  cvxsconn  36188  iscvm  36204  cvmliftlem5  36234  mpomulnzcnf  37279  rngohomval  39101  rngoisoval  39114  evlselv  43821  prjcrvfval  43871  rmxfval  44115  rmyfval  44116  mendplusg  44387  mendvsca  44392  mnringvald  45414  addrval  45650  subrval  45651  mulvval  45652  sigarval  48075  dmatALTval  49727  naryfval  49955  discsubc  50393  oppfvalg  50457  upfval  50507  setc1onsubc  50955  parhomval  50958  parhomidval  50961  lmdfval  51047  cmdfval  51048