Theorem ovres 6965

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 5305	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
2		fvres 6368	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩) = (𝐹‘⟨𝐴, 𝐵⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩) = (𝐹‘⟨𝐴, 𝐵⟩))
4		df-ov 6816	. 2 ⊢ (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩)
5		df-ov 6816	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
6	3, 4, 5	3eqtr4g 2819	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ⟨cop 4327   × cxp 5264   ↾ cres 5268  ‘cfv 6049  (class class class)co 6813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-xp 5272  df-res 5278  df-iota 6012  df-fv 6057  df-ov 6816

This theorem is referenced by:  ovresd  6966  oprres  6967  oprssov  6968  ofmresval  7075  cantnfval2  8739  mulnzcnopr  10865  prdsdsval3  16347  frmdplusg  17592  frmdadd  17593  grpissubg  17815  gaid  17932  gass  17934  gasubg  17935  mplsubrglem  19641  mamures  20398  mdetrlin  20610  mdetrsca  20611  pmatcollpw3lem  20790  tsmsxplem1  22157  tsmsxplem2  22158  xmetres2  22367  ressprdsds  22377  blres  22437  xmetresbl  22443  mscl  22467  xmscl  22468  xmsge0  22469  xmseq0  22470  nmfval2  22596  nmval2  22597  isngp3  22603  ngpds  22609  ngpocelbl  22709  xrsdsre  22814  divcn  22872  cncfmet  22912  cfilresi  23293  cfilres  23294  dvdsmulf1o  25119  sspgval  27893  sspsval  27895  sspmlem  27896  hhssabloilem  28427  hhssabloi  28428  hhssnv  28430  hhssmetdval  28444  raddcn  30284  xrge0pluscn  30295  cvmlift2lem9  31600  icoreval  33512  icoreelrnab  33513  equivbnd2  33904  ismtyres  33920  iccbnd  33952  exidreslem  33989  divrngcl  34069  isdrngo2  34070  rnghmresel  42474  rnghmsscmap2  42483  rnghmsscmap  42484  rnghmsubcsetclem2  42486  rngcifuestrc  42507  rhmresel  42520  rhmsscmap2  42529  rhmsscmap  42530  rhmsubcsetclem2  42532  rhmsscrnghm  42536  rhmsubcrngclem2  42538  rhmsubclem4  42599