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 5655	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
2	1	fvresd 6847	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩) = (𝐹‘⟨𝐴, 𝐵⟩))
3		df-ov 7359	. 2 ⊢ (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩)
4		df-ov 7359	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2799	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ⟨cop 4561   × cxp 5616   ↾ cres 5620  ‘cfv 6485  (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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-res 5630  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  ovresd  7523  oprres  7524  oprssov  7525  ofmresval  7636  cantnfval2  9581  mulnzcnf  11787  prdsdsval3  17439  mgmsscl  18604  frmdplusg  18813  frmdadd  18814  grpissubg  19113  gaid  19265  gass  19267  gasubg  19268  rnghmresel  20592  rnghmsscmap2  20601  rnghmsscmap  20602  rnghmsubcsetclem2  20604  rngcifuestrc  20611  rhmresel  20621  rhmsscmap2  20630  rhmsscmap  20631  rhmsubcsetclem2  20633  rhmsscrnghm  20637  rhmsubcrngclem2  20639  rhmsubclem4  20660  mplsubrglem  21978  mamures  22380  mdetrlin  22585  mdetrsca  22586  pmatcollpw3lem  22766  tsmsxplem1  24136  tsmsxplem2  24137  xmetres2  24344  ressprdsds  24354  blres  24414  xmetresbl  24420  mscl  24444  xmscl  24445  xmsge0  24446  xmseq0  24447  nmfval0  24573  nmval2  24575  isngp3  24581  ngpds  24587  ngpocelbl  24687  xrsdsre  24794  divcn  24853  cncfmet  24894  cfilresi  25280  cfilres  25281  mpodvdsmulf1o  27175  dvdsmulf1o  27177  zsoring  28419  sspgval  30818  sspsval  30820  sspmlem  30821  hhssabloilem  31350  hhssabloi  31351  hhssnv  31353  hhssmetdval  31366  raddcn  34113  xrge0pluscn  34124  cvmlift2lem9  35539  icoreval  37715  icoreelrnab  37716  equivbnd2  38159  ismtyres  38175  iccbnd  38207  exidreslem  38244  divrngcl  38324  isdrngo2  38325  ofoafo  43801  ofoacl  43802  naddcnfcl  43810  fuco11b  49827