Theorem ovres 7555

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4595   × cxp 5636   ↾ cres 5640  ‘cfv 6511  (class class class)co 7387

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-res 5650  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  ovresd  7556  oprres  7557  oprssov  7558  ofmresval  7669  cantnfval2  9622  mulnzcnf  11824  prdsdsval3  17448  mgmsscl  18572  frmdplusg  18781  frmdadd  18782  grpissubg  19078  gaid  19231  gass  19233  gasubg  19234  rnghmresel  20529  rnghmsscmap2  20538  rnghmsscmap  20539  rnghmsubcsetclem2  20541  rngcifuestrc  20548  rhmresel  20558  rhmsscmap2  20567  rhmsscmap  20568  rhmsubcsetclem2  20570  rhmsscrnghm  20574  rhmsubcrngclem2  20576  rhmsubclem4  20597  mplsubrglem  21913  mamures  22284  mdetrlin  22489  mdetrsca  22490  pmatcollpw3lem  22670  tsmsxplem1  24040  tsmsxplem2  24041  xmetres2  24249  ressprdsds  24259  blres  24319  xmetresbl  24325  mscl  24349  xmscl  24350  xmsge0  24351  xmseq0  24352  nmfval0  24478  nmval2  24480  isngp3  24486  ngpds  24492  ngpocelbl  24592  xrsdsre  24699  divcnOLD  24757  divcn  24759  cncfmet  24802  cfilresi  25195  cfilres  25196  mpodvdsmulf1o  27104  dvdsmulf1o  27106  sspgval  30658  sspsval  30660  sspmlem  30661  hhssabloilem  31190  hhssabloi  31191  hhssnv  31193  hhssmetdval  31206  raddcn  33919  xrge0pluscn  33930  cvmlift2lem9  35298  icoreval  37341  icoreelrnab  37342  equivbnd2  37786  ismtyres  37802  iccbnd  37834  exidreslem  37871  divrngcl  37951  isdrngo2  37952  ofoafo  43345  ofoacl  43346  naddcnfcl  43354  fuco11b  49326