Theorem ovres 7616

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ⟨cop 4654   × cxp 5698   ↾ cres 5702  ‘cfv 6573  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-res 5712  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  ovresd  7617  oprres  7618  oprssov  7619  ofmresval  7730  cantnfval2  9738  mulnzcnf  11936  prdsdsval3  17545  mgmsscl  18683  frmdplusg  18889  frmdadd  18890  grpissubg  19186  gaid  19339  gass  19341  gasubg  19342  rnghmresel  20642  rnghmsscmap2  20651  rnghmsscmap  20652  rnghmsubcsetclem2  20654  rngcifuestrc  20661  rhmresel  20671  rhmsscmap2  20680  rhmsscmap  20681  rhmsubcsetclem2  20683  rhmsscrnghm  20687  rhmsubcrngclem2  20689  rhmsubclem4  20710  mplsubrglem  22047  mamures  22422  mdetrlin  22629  mdetrsca  22630  pmatcollpw3lem  22810  tsmsxplem1  24182  tsmsxplem2  24183  xmetres2  24392  ressprdsds  24402  blres  24462  xmetresbl  24468  mscl  24492  xmscl  24493  xmsge0  24494  xmseq0  24495  nmfval0  24624  nmval2  24626  isngp3  24632  ngpds  24638  ngpocelbl  24746  xrsdsre  24851  divcnOLD  24909  divcn  24911  cncfmet  24954  cfilresi  25348  cfilres  25349  mpodvdsmulf1o  27255  dvdsmulf1o  27257  sspgval  30761  sspsval  30763  sspmlem  30764  hhssabloilem  31293  hhssabloi  31294  hhssnv  31296  hhssmetdval  31309  raddcn  33875  xrge0pluscn  33886  cvmlift2lem9  35279  icoreval  37319  icoreelrnab  37320  equivbnd2  37752  ismtyres  37768  iccbnd  37800  exidreslem  37837  divrngcl  37917  isdrngo2  37918  ofoafo  43318  ofoacl  43319  naddcnfcl  43327