Theorem ovres 7317

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ⟨cop 4576   × cxp 5556   ↾ cres 5560  ‘cfv 6358  (class class class)co 7159

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-xp 5564  df-res 5570  df-iota 6317  df-fv 6366  df-ov 7162

This theorem is referenced by:  ovresd  7318  oprres  7319  oprssov  7320  ofmresval  7425  cantnfval2  9135  mulnzcnopr  11289  prdsdsval3  16761  mgmsscl  17860  frmdplusg  18022  frmdadd  18023  grpissubg  18302  gaid  18432  gass  18434  gasubg  18435  mplsubrglem  20222  mamures  21004  mdetrlin  21214  mdetrsca  21215  pmatcollpw3lem  21394  tsmsxplem1  22764  tsmsxplem2  22765  xmetres2  22974  ressprdsds  22984  blres  23044  xmetresbl  23050  mscl  23074  xmscl  23075  xmsge0  23076  xmseq0  23077  nmfval2  23203  nmval2  23204  isngp3  23210  ngpds  23216  ngpocelbl  23316  xrsdsre  23421  divcn  23479  cncfmet  23519  cfilresi  23901  cfilres  23902  dvdsmulf1o  25774  sspgval  28509  sspsval  28511  sspmlem  28512  hhssabloilem  29041  hhssabloi  29042  hhssnv  29044  hhssmetdval  29057  raddcn  31176  xrge0pluscn  31187  cvmlift2lem9  32562  icoreval  34638  icoreelrnab  34639  equivbnd2  35074  ismtyres  35090  iccbnd  35122  exidreslem  35159  divrngcl  35239  isdrngo2  35240  rnghmresel  44242  rnghmsscmap2  44251  rnghmsscmap  44252  rnghmsubcsetclem2  44254  rngcifuestrc  44275  rhmresel  44288  rhmsscmap2  44297  rhmsscmap  44298  rhmsubcsetclem2  44300  rhmsscrnghm  44304  rhmsubcrngclem2  44306  rhmsubclem4  44367