Theorem ovres 7598

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ⟨cop 4636   × cxp 5686   ↾ cres 5690  ‘cfv 6562  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-res 5700  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  ovresd  7599  oprres  7600  oprssov  7601  ofmresval  7712  cantnfval2  9706  mulnzcnf  11906  prdsdsval3  17531  mgmsscl  18670  frmdplusg  18879  frmdadd  18880  grpissubg  19176  gaid  19329  gass  19331  gasubg  19332  rnghmresel  20636  rnghmsscmap2  20645  rnghmsscmap  20646  rnghmsubcsetclem2  20648  rngcifuestrc  20655  rhmresel  20665  rhmsscmap2  20674  rhmsscmap  20675  rhmsubcsetclem2  20677  rhmsscrnghm  20681  rhmsubcrngclem2  20683  rhmsubclem4  20704  mplsubrglem  22041  mamures  22416  mdetrlin  22623  mdetrsca  22624  pmatcollpw3lem  22804  tsmsxplem1  24176  tsmsxplem2  24177  xmetres2  24386  ressprdsds  24396  blres  24456  xmetresbl  24462  mscl  24486  xmscl  24487  xmsge0  24488  xmseq0  24489  nmfval0  24618  nmval2  24620  isngp3  24626  ngpds  24632  ngpocelbl  24740  xrsdsre  24845  divcnOLD  24903  divcn  24905  cncfmet  24948  cfilresi  25342  cfilres  25343  mpodvdsmulf1o  27251  dvdsmulf1o  27253  sspgval  30757  sspsval  30759  sspmlem  30760  hhssabloilem  31289  hhssabloi  31290  hhssnv  31292  hhssmetdval  31305  raddcn  33889  xrge0pluscn  33900  cvmlift2lem9  35295  icoreval  37335  icoreelrnab  37336  equivbnd2  37778  ismtyres  37794  iccbnd  37826  exidreslem  37863  divrngcl  37943  isdrngo2  37944  ofoafo  43345  ofoacl  43346  naddcnfcl  43354