Theorem ovres 7522

Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)

Assertion

Ref	Expression
ovres	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))

Proof of Theorem ovres

Step	Hyp	Ref	Expression
1		opelxpi 5659	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
2	1	fvresd 6852	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩) = (𝐹‘⟨𝐴, 𝐵⟩))
3		df-ov 7359	. 2 ⊢ (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩)
4		df-ov 7359	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2794	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ⟨cop 4584   × cxp 5620   ↾ cres 5624  ‘cfv 6490  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-res 5634  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  ovresd  7523  oprres  7524  oprssov  7525  ofmresval  7636  cantnfval2  9576  mulnzcnf  11781  prdsdsval3  17403  mgmsscl  18568  frmdplusg  18777  frmdadd  18778  grpissubg  19074  gaid  19226  gass  19228  gasubg  19229  rnghmresel  20551  rnghmsscmap2  20560  rnghmsscmap  20561  rnghmsubcsetclem2  20563  rngcifuestrc  20570  rhmresel  20580  rhmsscmap2  20589  rhmsscmap  20590  rhmsubcsetclem2  20592  rhmsscrnghm  20596  rhmsubcrngclem2  20598  rhmsubclem4  20619  mplsubrglem  21957  mamures  22339  mdetrlin  22544  mdetrsca  22545  pmatcollpw3lem  22725  tsmsxplem1  24095  tsmsxplem2  24096  xmetres2  24303  ressprdsds  24313  blres  24373  xmetresbl  24379  mscl  24403  xmscl  24404  xmsge0  24405  xmseq0  24406  nmfval0  24532  nmval2  24534  isngp3  24540  ngpds  24546  ngpocelbl  24646  xrsdsre  24753  divcnOLD  24811  divcn  24813  cncfmet  24856  cfilresi  25249  cfilres  25250  mpodvdsmulf1o  27158  dvdsmulf1o  27160  zsoring  28367  sspgval  30753  sspsval  30755  sspmlem  30756  hhssabloilem  31285  hhssabloi  31286  hhssnv  31288  hhssmetdval  31301  raddcn  34035  xrge0pluscn  34046  cvmlift2lem9  35454  icoreval  37497  icoreelrnab  37498  equivbnd2  37932  ismtyres  37948  iccbnd  37980  exidreslem  38017  divrngcl  38097  isdrngo2  38098  ofoafo  43540  ofoacl  43541  naddcnfcl  43549  fuco11b  49524