Theorem ovres 7588

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ⟨cop 4834   × cxp 5648   ↾ cres 5652  ‘cfv 6541  (class class class)co 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-res 5662  df-iota 6496  df-fv 6549  df-ov 7425

This theorem is used by:  ovresd  7589  oprres  7590  oprssov  7592  ofmresval  7711  cantnfval2  9675  mulnzcnf  11967  prdsdsval3  17663  mgmsscl  18828  frmdplusg  19057  frmdadd  19058  grpissubg  19364  gaid  19520  gass  19522  gasubg  19523  rnghmresel  20879  rnghmsscmap2  20888  rnghmsscmap  20889  rnghmsubcsetclem2  20891  rngcifuestrc  20898  rhmresel  20908  rhmsscmap2  20917  rhmsscmap  20918  rhmsubcsetclem2  20920  rhmsscrnghm  20924  rhmsubcrngclem2  20926  rhmsubclem4  20947  mplsubrglem  22318  mamures  22719  mdetrlin  22924  mdetrsca  22925  pmatcollpw3lem  23108  tsmsxplem1  24479  tsmsxplem2  24480  xmetres2  24687  ressprdsds  24697  blres  24757  xmetresbl  24763  mscl  24787  xmscl  24788  xmsge0  24789  xmseq0  24790  nmfval0  24916  nmval2  24918  isngp3  24924  ngpds  24930  ngpocelbl  25030  xrsdsre  25137  divcn  25196  cncfmet  25237  cfilresi  25623  cfilres  25624  mpodvdsmulf1o  27528  dvdsmulf1o  27530  zsoring  28802  sspgval  31338  sspsval  31340  sspmlem  31341  hhssabloilem  31870  hhssabloi  31871  hhssnv  31873  hhssmetdval  31886  raddcn  34609  xrge0pluscn  34620  cvmlift2lem9  36164  icoreval  38383  icoreelrnab  38384  equivbnd2  38833  ismtyres  38849  iccbnd  38881  exidreslem  38918  divrngcl  38998  isdrngo2  38999  ofoafo  44465  ofoacl  44466  naddcnfcl  44474  fuco11b  50566