Theorem ovres 7130

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ⟨cop 4447   × cxp 5405   ↾ cres 5409  ‘cfv 6188  (class class class)co 6976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-xp 5413  df-res 5419  df-iota 6152  df-fv 6196  df-ov 6979

This theorem is referenced by:  ovresd  7131  oprres  7132  oprssov  7133  ofmresval  7240  cantnfval2  8926  mulnzcnopr  11087  prdsdsval3  16614  frmdplusg  17860  frmdadd  17861  grpissubg  18083  gaid  18200  gass  18202  gasubg  18203  mplsubrglem  19933  mamures  20703  mdetrlin  20915  mdetrsca  20916  pmatcollpw3lem  21095  tsmsxplem1  22464  tsmsxplem2  22465  xmetres2  22674  ressprdsds  22684  blres  22744  xmetresbl  22750  mscl  22774  xmscl  22775  xmsge0  22776  xmseq0  22777  nmfval2  22903  nmval2  22904  isngp3  22910  ngpds  22916  ngpocelbl  23016  xrsdsre  23121  divcn  23179  cncfmet  23219  cfilresi  23601  cfilres  23602  dvdsmulf1o  25473  sspgval  28283  sspsval  28285  sspmlem  28286  hhssabloilem  28817  hhssabloi  28818  hhssnv  28820  hhssmetdval  28834  raddcn  30822  xrge0pluscn  30833  cvmlift2lem9  32149  icoreval  34082  icoreelrnab  34083  equivbnd2  34518  ismtyres  34534  iccbnd  34566  exidreslem  34603  divrngcl  34683  isdrngo2  34684  rnghmresel  43605  rnghmsscmap2  43614  rnghmsscmap  43615  rnghmsubcsetclem2  43617  rngcifuestrc  43638  rhmresel  43651  rhmsscmap2  43660  rhmsscmap  43661  rhmsubcsetclem2  43663  rhmsscrnghm  43667  rhmsubcrngclem2  43669  rhmsubclem4  43730