Theorem ovres 6945

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 5286	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
2		fvres 6346	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩) = (𝐹‘⟨𝐴, 𝐵⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩) = (𝐹‘⟨𝐴, 𝐵⟩))
4		df-ov 6794	. 2 ⊢ (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩)
5		df-ov 6794	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
6	3, 4, 5	3eqtr4g 2830	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ⟨cop 4322   × cxp 5247   ↾ cres 5251  ‘cfv 6029  (class class class)co 6791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-xp 5255  df-res 5261  df-iota 5992  df-fv 6037  df-ov 6794

This theorem is referenced by:  ovresd  6946  oprres  6947  oprssov  6948  ofmresval  7055  cantnfval2  8728  mulnzcnopr  10873  prdsdsval3  16346  frmdplusg  17592  frmdadd  17593  grpissubg  17815  gaid  17932  gass  17934  gasubg  17935  mplsubrglem  19647  mamures  20406  mdetrlin  20619  mdetrsca  20620  pmatcollpw3lem  20801  tsmsxplem1  22169  tsmsxplem2  22170  xmetres2  22379  ressprdsds  22389  blres  22449  xmetresbl  22455  mscl  22479  xmscl  22480  xmsge0  22481  xmseq0  22482  nmfval2  22608  nmval2  22609  isngp3  22615  ngpds  22621  ngpocelbl  22721  xrsdsre  22826  divcn  22884  cncfmet  22924  cfilresi  23305  cfilres  23306  dvdsmulf1o  25134  sspgval  27917  sspsval  27919  sspmlem  27920  hhssabloilem  28451  hhssabloi  28452  hhssnv  28454  hhssmetdval  28468  raddcn  30308  xrge0pluscn  30319  cvmlift2lem9  31624  icoreval  33531  icoreelrnab  33532  equivbnd2  33916  ismtyres  33932  iccbnd  33964  exidreslem  34001  divrngcl  34081  isdrngo2  34082  rnghmresel  42485  rnghmsscmap2  42494  rnghmsscmap  42495  rnghmsubcsetclem2  42497  rngcifuestrc  42518  rhmresel  42531  rhmsscmap2  42540  rhmsscmap  42541  rhmsubcsetclem2  42543  rhmsscrnghm  42547  rhmsubcrngclem2  42549  rhmsubclem4  42610