Theorem ovres 7526

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4574   × cxp 5622   ↾ cres 5626  ‘cfv 6492  (class class class)co 7360

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-res 5636  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  ovresd  7527  oprres  7528  oprssov  7529  ofmresval  7640  cantnfval2  9581  mulnzcnf  11787  prdsdsval3  17439  mgmsscl  18604  frmdplusg  18813  frmdadd  18814  grpissubg  19113  gaid  19265  gass  19267  gasubg  19268  rnghmresel  20588  rnghmsscmap2  20597  rnghmsscmap  20598  rnghmsubcsetclem2  20600  rngcifuestrc  20607  rhmresel  20617  rhmsscmap2  20626  rhmsscmap  20627  rhmsubcsetclem2  20629  rhmsscrnghm  20633  rhmsubcrngclem2  20635  rhmsubclem4  20656  mplsubrglem  21992  mamures  22372  mdetrlin  22577  mdetrsca  22578  pmatcollpw3lem  22758  tsmsxplem1  24128  tsmsxplem2  24129  xmetres2  24336  ressprdsds  24346  blres  24406  xmetresbl  24412  mscl  24436  xmscl  24437  xmsge0  24438  xmseq0  24439  nmfval0  24565  nmval2  24567  isngp3  24573  ngpds  24579  ngpocelbl  24679  xrsdsre  24786  divcn  24845  cncfmet  24886  cfilresi  25272  cfilres  25273  mpodvdsmulf1o  27171  dvdsmulf1o  27173  zsoring  28415  sspgval  30815  sspsval  30817  sspmlem  30818  hhssabloilem  31347  hhssabloi  31348  hhssnv  31350  hhssmetdval  31363  raddcn  34089  xrge0pluscn  34100  cvmlift2lem9  35509  icoreval  37683  icoreelrnab  37684  equivbnd2  38127  ismtyres  38143  iccbnd  38175  exidreslem  38212  divrngcl  38292  isdrngo2  38293  ofoafo  43802  ofoacl  43803  naddcnfcl  43811  fuco11b  49824