Theorem ovres 6698

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ⟨cop 4131   × cxp 5036   ↾ cres 5040  ‘cfv 5804  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-xp 5044  df-res 5050  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  ovresd  6699  oprres  6700  oprssov  6701  ofmresval  6808  cantnfval2  8449  mulnzcnopr  10552  prdsdsval3  15968  frmdplusg  17214  frmdadd  17215  grpissubg  17437  gaid  17555  gass  17557  gasubg  17558  mplsubrglem  19260  mamures  20015  mdetrlin  20227  mdetrsca  20228  pmatcollpw3lem  20407  tsmsxplem1  21766  tsmsxplem2  21767  xmetres2  21976  ressprdsds  21986  blres  22046  xmetresbl  22052  mscl  22076  xmscl  22077  xmsge0  22078  xmseq0  22079  nmfval2  22205  nmval2  22206  isngp3  22212  ngpds  22218  ngpocelbl  22318  xrsdsre  22421  divcn  22479  cncfmet  22519  cfilresi  22901  cfilres  22902  dvdsmulf1o  24720  sspgval  26968  sspsval  26970  sspmlem  26971  hhssabloilem  27502  hhssabloi  27503  hhssnv  27505  hhssmetdval  27519  raddcn  29303  xrge0pluscn  29314  cvmlift2lem9  30547  icoreval  32377  icoreelrnab  32378  equivbnd2  32761  ismtyres  32777  iccbnd  32809  exidreslem  32846  divrngcl  32926  isdrngo2  32927  rnghmresel  41756  rnghmsscmap2  41765  rnghmsscmap  41766  rnghmsubcsetclem2  41768  rngcifuestrc  41789  rhmresel  41802  rhmsscmap2  41811  rhmsscmap  41812  rhmsubcsetclem2  41814  rhmsscrnghm  41818  rhmsubcrngclem2  41820  rhmsubclem4  41881