Theorem ovres 7576

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ⟨cop 4595   × cxp 5659   ↾ cres 5663  ‘cfv 6536  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-res 5673  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  ovresd  7577  oprres  7578  oprssov  7579  ofmresval  7690  cantnfval2  9634  mulnzcnf  11855  prdsdsval3  17533  mgmsscl  18698  frmdplusg  18908  frmdadd  18909  grpissubg  19208  gaid  19364  gass  19366  gasubg  19367  rnghmresel  20719  rnghmsscmap2  20728  rnghmsscmap  20729  rnghmsubcsetclem2  20731  rngcifuestrc  20738  rhmresel  20748  rhmsscmap2  20757  rhmsscmap  20758  rhmsubcsetclem2  20760  rhmsscrnghm  20764  rhmsubcrngclem2  20766  rhmsubclem4  20787  mplsubrglem  22153  mamures  22554  mdetrlin  22759  mdetrsca  22760  pmatcollpw3lem  22940  tsmsxplem1  24310  tsmsxplem2  24311  xmetres2  24518  ressprdsds  24528  blres  24588  xmetresbl  24594  mscl  24618  xmscl  24619  xmsge0  24620  xmseq0  24621  nmfval0  24747  nmval2  24749  isngp3  24755  ngpds  24761  ngpocelbl  24861  xrsdsre  24968  divcn  25027  cncfmet  25068  cfilresi  25454  cfilres  25455  mpodvdsmulf1o  27358  dvdsmulf1o  27360  zsoring  28602  sspgval  31081  sspsval  31083  sspmlem  31084  hhssabloilem  31613  hhssabloi  31614  hhssnv  31616  hhssmetdval  31629  raddcn  34319  xrge0pluscn  34330  cvmlift2lem9  35803  icoreval  37999  icoreelrnab  38000  equivbnd2  38443  ismtyres  38459  iccbnd  38491  exidreslem  38528  divrngcl  38608  isdrngo2  38609  ofoafo  44083  ofoacl  44084  naddcnfcl  44092  fuco11b  50115