Theorem ovres 7524

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ⟨cop 4586   × cxp 5622   ↾ cres 5626  ‘cfv 6492  (class class class)co 7358

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-res 5636  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  ovresd  7525  oprres  7526  oprssov  7527  ofmresval  7638  cantnfval2  9578  mulnzcnf  11783  prdsdsval3  17405  mgmsscl  18570  frmdplusg  18779  frmdadd  18780  grpissubg  19076  gaid  19228  gass  19230  gasubg  19231  rnghmresel  20553  rnghmsscmap2  20562  rnghmsscmap  20563  rnghmsubcsetclem2  20565  rngcifuestrc  20572  rhmresel  20582  rhmsscmap2  20591  rhmsscmap  20592  rhmsubcsetclem2  20594  rhmsscrnghm  20598  rhmsubcrngclem2  20600  rhmsubclem4  20621  mplsubrglem  21959  mamures  22341  mdetrlin  22546  mdetrsca  22547  pmatcollpw3lem  22727  tsmsxplem1  24097  tsmsxplem2  24098  xmetres2  24305  ressprdsds  24315  blres  24375  xmetresbl  24381  mscl  24405  xmscl  24406  xmsge0  24407  xmseq0  24408  nmfval0  24534  nmval2  24536  isngp3  24542  ngpds  24548  ngpocelbl  24648  xrsdsre  24755  divcnOLD  24813  divcn  24815  cncfmet  24858  cfilresi  25251  cfilres  25252  mpodvdsmulf1o  27160  dvdsmulf1o  27162  zsoring  28405  sspgval  30804  sspsval  30806  sspmlem  30807  hhssabloilem  31336  hhssabloi  31337  hhssnv  31339  hhssmetdval  31352  raddcn  34086  xrge0pluscn  34097  cvmlift2lem9  35505  icoreval  37558  icoreelrnab  37559  equivbnd2  37993  ismtyres  38009  iccbnd  38041  exidreslem  38078  divrngcl  38158  isdrngo2  38159  ofoafo  43598  ofoacl  43599  naddcnfcl  43607  fuco11b  49582