Theorem ovres 7507

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ⟨cop 4577   × cxp 5609   ↾ cres 5613  ‘cfv 6476  (class class class)co 7341

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-xp 5617  df-res 5623  df-iota 6432  df-fv 6484  df-ov 7344

This theorem is referenced by:  ovresd  7508  oprres  7509  oprssov  7510  ofmresval  7621  cantnfval2  9554  mulnzcnf  11758  prdsdsval3  17384  mgmsscl  18548  frmdplusg  18757  frmdadd  18758  grpissubg  19054  gaid  19206  gass  19208  gasubg  19209  rnghmresel  20530  rnghmsscmap2  20539  rnghmsscmap  20540  rnghmsubcsetclem2  20542  rngcifuestrc  20549  rhmresel  20559  rhmsscmap2  20568  rhmsscmap  20569  rhmsubcsetclem2  20571  rhmsscrnghm  20575  rhmsubcrngclem2  20577  rhmsubclem4  20598  mplsubrglem  21936  mamures  22307  mdetrlin  22512  mdetrsca  22513  pmatcollpw3lem  22693  tsmsxplem1  24063  tsmsxplem2  24064  xmetres2  24271  ressprdsds  24281  blres  24341  xmetresbl  24347  mscl  24371  xmscl  24372  xmsge0  24373  xmseq0  24374  nmfval0  24500  nmval2  24502  isngp3  24508  ngpds  24514  ngpocelbl  24614  xrsdsre  24721  divcnOLD  24779  divcn  24781  cncfmet  24824  cfilresi  25217  cfilres  25218  mpodvdsmulf1o  27126  dvdsmulf1o  27128  zsoring  28327  sspgval  30701  sspsval  30703  sspmlem  30704  hhssabloilem  31233  hhssabloi  31234  hhssnv  31236  hhssmetdval  31249  raddcn  33934  xrge0pluscn  33945  cvmlift2lem9  35347  icoreval  37387  icoreelrnab  37388  equivbnd2  37832  ismtyres  37848  iccbnd  37880  exidreslem  37917  divrngcl  37997  isdrngo2  37998  ofoafo  43389  ofoacl  43390  naddcnfcl  43398  fuco11b  49369