Theorem ovres 7618

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ⟨cop 4840   × cxp 5656   ↾ cres 5660  ‘cfv 6566  (class class class)co 7451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-res 5670  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  ovresd  7619  oprres  7620  oprssov  7622  ofmresval  7741  cantnfval2  9707  mulnzcnf  12002  prdsdsval3  17706  mgmsscl  18871  frmdplusg  19100  frmdadd  19101  grpissubg  19407  gaid  19564  gass  19566  gasubg  19567  rnghmresel  20923  rnghmsscmap2  20932  rnghmsscmap  20933  rnghmsubcsetclem2  20935  rngcifuestrc  20942  rhmresel  20952  rhmsscmap2  20961  rhmsscmap  20962  rhmsubcsetclem2  20964  rhmsscrnghm  20968  rhmsubcrngclem2  20970  rhmsubclem4  20991  mplsubrglem  22366  mamures  22767  mdetrlin  22972  mdetrsca  22973  pmatcollpw3lem  23156  tsmsxplem1  24527  tsmsxplem2  24528  xmetres2  24735  ressprdsds  24745  blres  24805  xmetresbl  24811  mscl  24835  xmscl  24836  xmsge0  24837  xmseq0  24838  nmfval0  24964  nmval2  24966  isngp3  24972  ngpds  24978  ngpocelbl  25078  xrsdsre  25185  divcn  25244  cncfmet  25285  cfilresi  25671  cfilres  25672  mpodvdsmulf1o  27578  dvdsmulf1o  27580  zsoring  28852  sspgval  31388  sspsval  31390  sspmlem  31391  hhssabloilem  31920  hhssabloi  31921  hhssnv  31923  hhssmetdval  31936  raddcn  34672  xrge0pluscn  34683  cvmlift2lem9  36284  icoreval  38544  icoreelrnab  38545  equivbnd2  38992  ismtyres  39008  iccbnd  39040  exidreslem  39077  divrngcl  39157  isdrngo2  39158  ofoafo  44619  ofoacl  44620  naddcnfcl  44628  fuco11b  50790