Theorem ovres 7521

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ⟨cop 4583   × cxp 5619   ↾ cres 5623  ‘cfv 6489  (class class class)co 7355

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 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2712  df-cleq 2725  df-clel 2808  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 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-xp 5627  df-res 5633  df-iota 6445  df-fv 6497  df-ov 7358

This theorem is referenced by:  ovresd  7522  oprres  7523  oprssov  7524  ofmresval  7635  cantnfval2  9569  mulnzcnf  11773  prdsdsval3  17399  mgmsscl  18563  frmdplusg  18772  frmdadd  18773  grpissubg  19069  gaid  19221  gass  19223  gasubg  19224  rnghmresel  20545  rnghmsscmap2  20554  rnghmsscmap  20555  rnghmsubcsetclem2  20557  rngcifuestrc  20564  rhmresel  20574  rhmsscmap2  20583  rhmsscmap  20584  rhmsubcsetclem2  20586  rhmsscrnghm  20590  rhmsubcrngclem2  20592  rhmsubclem4  20613  mplsubrglem  21951  mamures  22322  mdetrlin  22527  mdetrsca  22528  pmatcollpw3lem  22708  tsmsxplem1  24078  tsmsxplem2  24079  xmetres2  24286  ressprdsds  24296  blres  24356  xmetresbl  24362  mscl  24386  xmscl  24387  xmsge0  24388  xmseq0  24389  nmfval0  24515  nmval2  24517  isngp3  24523  ngpds  24529  ngpocelbl  24629  xrsdsre  24736  divcnOLD  24794  divcn  24796  cncfmet  24839  cfilresi  25232  cfilres  25233  mpodvdsmulf1o  27141  dvdsmulf1o  27143  zsoring  28342  sspgval  30720  sspsval  30722  sspmlem  30723  hhssabloilem  31252  hhssabloi  31253  hhssnv  31255  hhssmetdval  31268  raddcn  33953  xrge0pluscn  33964  cvmlift2lem9  35366  icoreval  37408  icoreelrnab  37409  equivbnd2  37842  ismtyres  37858  iccbnd  37890  exidreslem  37927  divrngcl  38007  isdrngo2  38008  ofoafo  43463  ofoacl  43464  naddcnfcl  43472  fuco11b  49452