Theorem ovres 7579

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ⟨cop 4590   × cxp 5653   ↾ cres 5657  ‘cfv 6533  (class class class)co 7413

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-res 5667  df-iota 6489  df-fv 6541  df-ov 7416

This theorem is used by:  ovresd  7580  oprres  7581  oprssov  7583  ofmresval  7694  cantnfval2  9648  mulnzcnf  11884  prdsdsval3  17570  mgmsscl  18735  frmdplusg  18963  frmdadd  18964  grpissubg  19270  gaid  19426  gass  19428  gasubg  19429  rnghmresel  20782  rnghmsscmap2  20791  rnghmsscmap  20792  rnghmsubcsetclem2  20794  rngcifuestrc  20801  rhmresel  20811  rhmsscmap2  20820  rhmsscmap  20821  rhmsubcsetclem2  20823  rhmsscrnghm  20827  rhmsubcrngclem2  20829  rhmsubclem4  20850  mplsubrglem  22218  mamures  22619  mdetrlin  22824  mdetrsca  22825  pmatcollpw3lem  23008  tsmsxplem1  24379  tsmsxplem2  24380  xmetres2  24587  ressprdsds  24597  blres  24657  xmetresbl  24663  mscl  24687  xmscl  24688  xmsge0  24689  xmseq0  24690  nmfval0  24816  nmval2  24818  isngp3  24824  ngpds  24830  ngpocelbl  24930  xrsdsre  25037  divcn  25096  cncfmet  25137  cfilresi  25523  cfilres  25524  mpodvdsmulf1o  27430  dvdsmulf1o  27432  zsoring  28674  sspgval  31210  sspsval  31212  sspmlem  31213  hhssabloilem  31742  hhssabloi  31743  hhssnv  31745  hhssmetdval  31758  raddcn  34439  xrge0pluscn  34450  cvmlift2lem9  35890  icoreval  38107  icoreelrnab  38108  equivbnd2  38542  ismtyres  38558  iccbnd  38590  exidreslem  38627  divrngcl  38707  isdrngo2  38708  ofoafo  44197  ofoacl  44198  naddcnfcl  44206  fuco11b  50263