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 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455  (class class class)co 7412   ∈ cmpo 7414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417

This theorem is referenced by:  ovmpot  7573  1st2val  8015  2nd2val  8016  mptmpoopabbrd  8079  cantnffval  9633  cantnfsuc  9640  fseqenlem1  10009  xaddval  13250  xmulval  13252  fzoval  13690  expval  14101  ccatfval  14612  splcl  14791  cshfn  14829  bpolylem  16103  ruclem1  16288  sadfval  16511  sadcp1  16514  smufval  16536  smupp1  16539  eucalgval2  16640  pcval  16905  pc0  16915  vdwapval  17034  pwsval  17540  xpsfval  17621  xpsval  17625  rescval  17885  isfunc  17922  isfull  17970  isfth  17974  natfval  18007  catcisolem  18168  xpchom  18237  1stfval  18248  2ndfval  18251  yonedalem3a  18331  yonedainv  18338  plusfval  18706  ismgmhm  18755  ismhm  18844  mulgval  19138  eqgfval  19245  isghm  19287  isga  19362  subgga  19371  cayleylem1  19483  sylow1lem2  19670  isslw  19679  sylow2blem1  19691  sylow3lem1  19698  sylow3lem6  19703  frgpuptinv  19842  frgpup2  19847  isrhm  20561  scafval  20983  islmhm  21129  xrsdsval  21542  ipfval  21780  dsmmval  21865  psrmulfval  22074  mplval  22119  ltbval  22175  mpfrcl  22217  evlsval  22218  evlval  22232  mhpfval  22282  matval  22549  submafval  22717  mdetfval  22724  minmar1fval  22784  txval  23702  xkoval  23725  hmeofval  23896  flffval  24127  qustgplem  24259  dscmet  24710  dscopn  24711  tngval  24777  nmofval  24852  nghmfval  24860  isnmhm  24884  htpyco1  25118  htpycc  25120  phtpycc  25131  reparphti  25137  pcoval  25151  pcohtpylem  25159  pcorevlem  25166  dyadval  25732  itg1addlem3  25838  itg1addlem4  25839  mbfi1fseqlem3  25857  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mbfi1fseqlem6  25860  mdegfval  26200  quotval  26434  elqaalem2  26462  cxpval  26810  cxpcn3  26894  angval  26947  sgmval  27287  lgsval  27446  wwlksn  30167  wspthsn  30178  rusgrnumwwlklem  30303  clwwlkn  30358  2clwwlk  30679  numclwwlkovh0  30704  numclwwlkovq  30706  shsval  31645  sshjval  31683  faeval  34617  txsconnlem  35713  cvxsconn  35716  iscvm  35732  cvmliftlem5  35762  mpomulnzcnf  36792  rngohomval  38596  rngoisoval  38609  evlselv  43304  prjcrvfval  43346  rmxfval  43614  rmyfval  43615  mendplusg  43892  mendvsca  43897  mnringvald  44920  addrval  45157  subrval  45158  mulvval  45159  sigarval  47547  dmatALTval  49163  naryfval  49391  discsubc  49825  oppfvalg  49887  upfval  49937  setc1onsubc  50363  lmdfval  50410  cmdfval  50411