Theorem ovres 7416

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ⟨cop 4564   × cxp 5578   ↾ cres 5582  ‘cfv 6418  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-res 5592  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  ovresd  7417  oprres  7418  oprssov  7419  ofmresval  7527  cantnfval2  9357  mulnzcnopr  11551  prdsdsval3  17113  mgmsscl  18246  frmdplusg  18408  frmdadd  18409  grpissubg  18690  gaid  18820  gass  18822  gasubg  18823  mplsubrglem  21120  mamures  21449  mdetrlin  21659  mdetrsca  21660  pmatcollpw3lem  21840  tsmsxplem1  23212  tsmsxplem2  23213  xmetres2  23422  ressprdsds  23432  blres  23492  xmetresbl  23498  mscl  23522  xmscl  23523  xmsge0  23524  xmseq0  23525  nmfval0  23652  nmval2  23654  isngp3  23660  ngpds  23666  ngpocelbl  23774  xrsdsre  23879  divcn  23937  cncfmet  23978  cfilresi  24364  cfilres  24365  dvdsmulf1o  26248  sspgval  28992  sspsval  28994  sspmlem  28995  hhssabloilem  29524  hhssabloi  29525  hhssnv  29527  hhssmetdval  29540  raddcn  31781  xrge0pluscn  31792  cvmlift2lem9  33173  icoreval  35451  icoreelrnab  35452  equivbnd2  35877  ismtyres  35893  iccbnd  35925  exidreslem  35962  divrngcl  36042  isdrngo2  36043  rnghmresel  45410  rnghmsscmap2  45419  rnghmsscmap  45420  rnghmsubcsetclem2  45422  rngcifuestrc  45443  rhmresel  45456  rhmsscmap2  45465  rhmsscmap  45466  rhmsubcsetclem2  45468  rhmsscrnghm  45472  rhmsubcrngclem2  45474  rhmsubclem4  45535