Theorem ovres 7479

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ⟨cop 4576   × cxp 5605   ↾ cres 5609  ‘cfv 6465  (class class class)co 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-xp 5613  df-res 5619  df-iota 6417  df-fv 6473  df-ov 7319

This theorem is referenced by:  ovresd  7480  oprres  7481  oprssov  7482  ofmresval  7590  cantnfval2  9504  mulnzcnopr  11700  prdsdsval3  17270  mgmsscl  18405  frmdplusg  18566  frmdadd  18567  grpissubg  18848  gaid  18978  gass  18980  gasubg  18981  mplsubrglem  21290  mamures  21619  mdetrlin  21831  mdetrsca  21832  pmatcollpw3lem  22012  tsmsxplem1  23384  tsmsxplem2  23385  xmetres2  23594  ressprdsds  23604  blres  23664  xmetresbl  23670  mscl  23694  xmscl  23695  xmsge0  23696  xmseq0  23697  nmfval0  23826  nmval2  23828  isngp3  23834  ngpds  23840  ngpocelbl  23948  xrsdsre  24053  divcn  24111  cncfmet  24152  cfilresi  24539  cfilres  24540  dvdsmulf1o  26423  sspgval  29223  sspsval  29225  sspmlem  29226  hhssabloilem  29755  hhssabloi  29756  hhssnv  29758  hhssmetdval  29771  raddcn  32015  xrge0pluscn  32026  cvmlift2lem9  33408  icoreval  35601  icoreelrnab  35602  equivbnd2  36027  ismtyres  36043  iccbnd  36075  exidreslem  36112  divrngcl  36192  isdrngo2  36193  ofoafo  41273  ofoacl  41274  naddcnfcl  41282  rnghmresel  45792  rnghmsscmap2  45801  rnghmsscmap  45802  rnghmsubcsetclem2  45804  rngcifuestrc  45825  rhmresel  45838  rhmsscmap2  45847  rhmsscmap  45848  rhmsubcsetclem2  45850  rhmsscrnghm  45854  rhmsubcrngclem2  45856  rhmsubclem4  45917