Theorem ovres 7438

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ⟨cop 4567   × cxp 5587   ↾ cres 5591  ‘cfv 6433  (class class class)co 7275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-res 5601  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  ovresd  7439  oprres  7440  oprssov  7441  ofmresval  7549  cantnfval2  9427  mulnzcnopr  11621  prdsdsval3  17196  mgmsscl  18331  frmdplusg  18493  frmdadd  18494  grpissubg  18775  gaid  18905  gass  18907  gasubg  18908  mplsubrglem  21210  mamures  21539  mdetrlin  21751  mdetrsca  21752  pmatcollpw3lem  21932  tsmsxplem1  23304  tsmsxplem2  23305  xmetres2  23514  ressprdsds  23524  blres  23584  xmetresbl  23590  mscl  23614  xmscl  23615  xmsge0  23616  xmseq0  23617  nmfval0  23746  nmval2  23748  isngp3  23754  ngpds  23760  ngpocelbl  23868  xrsdsre  23973  divcn  24031  cncfmet  24072  cfilresi  24459  cfilres  24460  dvdsmulf1o  26343  sspgval  29091  sspsval  29093  sspmlem  29094  hhssabloilem  29623  hhssabloi  29624  hhssnv  29626  hhssmetdval  29639  raddcn  31879  xrge0pluscn  31890  cvmlift2lem9  33273  icoreval  35524  icoreelrnab  35525  equivbnd2  35950  ismtyres  35966  iccbnd  35998  exidreslem  36035  divrngcl  36115  isdrngo2  36116  rnghmresel  45522  rnghmsscmap2  45531  rnghmsscmap  45532  rnghmsubcsetclem2  45534  rngcifuestrc  45555  rhmresel  45568  rhmsscmap2  45577  rhmsscmap  45578  rhmsubcsetclem2  45580  rhmsscrnghm  45584  rhmsubcrngclem2  45586  rhmsubclem4  45647