Theorem ovres 7525

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ⟨cop 4597   × cxp 5636   ↾ cres 5640  ‘cfv 6501  (class class class)co 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-res 5650  df-iota 6453  df-fv 6509  df-ov 7365

This theorem is referenced by:  ovresd  7526  oprres  7527  oprssov  7528  ofmresval  7638  cantnfval2  9614  mulnzcnopr  11810  prdsdsval3  17381  mgmsscl  18516  frmdplusg  18678  frmdadd  18679  grpissubg  18962  gaid  19093  gass  19095  gasubg  19096  mplsubrglem  21447  mamures  21776  mdetrlin  21988  mdetrsca  21989  pmatcollpw3lem  22169  tsmsxplem1  23541  tsmsxplem2  23542  xmetres2  23751  ressprdsds  23761  blres  23821  xmetresbl  23827  mscl  23851  xmscl  23852  xmsge0  23853  xmseq0  23854  nmfval0  23983  nmval2  23985  isngp3  23991  ngpds  23997  ngpocelbl  24105  xrsdsre  24210  divcn  24268  cncfmet  24309  cfilresi  24696  cfilres  24697  dvdsmulf1o  26580  sspgval  29734  sspsval  29736  sspmlem  29737  hhssabloilem  30266  hhssabloi  30267  hhssnv  30269  hhssmetdval  30282  raddcn  32599  xrge0pluscn  32610  cvmlift2lem9  33992  icoreval  35897  icoreelrnab  35898  equivbnd2  36324  ismtyres  36340  iccbnd  36372  exidreslem  36409  divrngcl  36489  isdrngo2  36490  ofoafo  41749  ofoacl  41750  naddcnfcl  41758  rnghmresel  46382  rnghmsscmap2  46391  rnghmsscmap  46392  rnghmsubcsetclem2  46394  rngcifuestrc  46415  rhmresel  46428  rhmsscmap2  46437  rhmsscmap  46438  rhmsubcsetclem2  46440  rhmsscrnghm  46444  rhmsubcrngclem2  46446  rhmsubclem4  46507