Theorem ovres 7599

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ⟨cop 4632   × cxp 5683   ↾ cres 5687  ‘cfv 6561  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-res 5697  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  ovresd  7600  oprres  7601  oprssov  7602  ofmresval  7713  cantnfval2  9709  mulnzcnf  11909  prdsdsval3  17530  mgmsscl  18658  frmdplusg  18867  frmdadd  18868  grpissubg  19164  gaid  19317  gass  19319  gasubg  19320  rnghmresel  20620  rnghmsscmap2  20629  rnghmsscmap  20630  rnghmsubcsetclem2  20632  rngcifuestrc  20639  rhmresel  20649  rhmsscmap2  20658  rhmsscmap  20659  rhmsubcsetclem2  20661  rhmsscrnghm  20665  rhmsubcrngclem2  20667  rhmsubclem4  20688  mplsubrglem  22024  mamures  22401  mdetrlin  22608  mdetrsca  22609  pmatcollpw3lem  22789  tsmsxplem1  24161  tsmsxplem2  24162  xmetres2  24371  ressprdsds  24381  blres  24441  xmetresbl  24447  mscl  24471  xmscl  24472  xmsge0  24473  xmseq0  24474  nmfval0  24603  nmval2  24605  isngp3  24611  ngpds  24617  ngpocelbl  24725  xrsdsre  24832  divcnOLD  24890  divcn  24892  cncfmet  24935  cfilresi  25329  cfilres  25330  mpodvdsmulf1o  27237  dvdsmulf1o  27239  sspgval  30748  sspsval  30750  sspmlem  30751  hhssabloilem  31280  hhssabloi  31281  hhssnv  31283  hhssmetdval  31296  raddcn  33928  xrge0pluscn  33939  cvmlift2lem9  35316  icoreval  37354  icoreelrnab  37355  equivbnd2  37799  ismtyres  37815  iccbnd  37847  exidreslem  37884  divrngcl  37964  isdrngo2  37965  ofoafo  43369  ofoacl  43370  naddcnfcl  43378  fuco11b  49032