Theorem ovres 7557

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ⟨cop 4585   × cxp 5641   ↾ cres 5645  ‘cfv 6516  (class class class)co 7391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-xp 5649  df-res 5655  df-iota 6472  df-fv 6524  df-ov 7394

This theorem is referenced by:  ovresd  7558  oprres  7559  oprssov  7560  ofmresval  7671  cantnfval2  9618  mulnzcnf  11827  prdsdsval3  17505  mgmsscl  18670  frmdplusg  18879  frmdadd  18880  grpissubg  19179  gaid  19330  gass  19332  gasubg  19333  rnghmresel  20657  rnghmsscmap2  20666  rnghmsscmap  20667  rnghmsubcsetclem2  20669  rngcifuestrc  20676  rhmresel  20686  rhmsscmap2  20695  rhmsscmap  20696  rhmsubcsetclem2  20698  rhmsscrnghm  20702  rhmsubcrngclem2  20704  rhmsubclem4  20725  mplsubrglem  22043  mamures  22445  mdetrlin  22650  mdetrsca  22651  pmatcollpw3lem  22831  tsmsxplem1  24201  tsmsxplem2  24202  xmetres2  24409  ressprdsds  24419  blres  24479  xmetresbl  24485  mscl  24509  xmscl  24510  xmsge0  24511  xmseq0  24512  nmfval0  24638  nmval2  24640  isngp3  24646  ngpds  24652  ngpocelbl  24752  xrsdsre  24859  divcn  24918  cncfmet  24959  cfilresi  25345  cfilres  25346  mpodvdsmulf1o  27246  dvdsmulf1o  27248  zsoring  28490  sspgval  30889  sspsval  30891  sspmlem  30892  hhssabloilem  31421  hhssabloi  31422  hhssnv  31424  hhssmetdval  31437  raddcn  34187  xrge0pluscn  34198  cvmlift2lem9  35622  icoreval  37808  icoreelrnab  37809  equivbnd2  38252  ismtyres  38268  iccbnd  38300  exidreslem  38337  divrngcl  38417  isdrngo2  38418  ofoafo  43894  ofoacl  43895  naddcnfcl  43903  fuco11b  49919