Theorem ovres 7352

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ⟨cop 4533   × cxp 5534   ↾ cres 5538  ‘cfv 6358  (class class class)co 7191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-xp 5542  df-res 5548  df-iota 6316  df-fv 6366  df-ov 7194

This theorem is referenced by:  ovresd  7353  oprres  7354  oprssov  7355  ofmresval  7462  cantnfval2  9262  mulnzcnopr  11443  prdsdsval3  16944  mgmsscl  18073  frmdplusg  18235  frmdadd  18236  grpissubg  18517  gaid  18647  gass  18649  gasubg  18650  mplsubrglem  20920  mamures  21243  mdetrlin  21453  mdetrsca  21454  pmatcollpw3lem  21634  tsmsxplem1  23004  tsmsxplem2  23005  xmetres2  23213  ressprdsds  23223  blres  23283  xmetresbl  23289  mscl  23313  xmscl  23314  xmsge0  23315  xmseq0  23316  nmfval0  23442  nmval2  23444  isngp3  23450  ngpds  23456  ngpocelbl  23556  xrsdsre  23661  divcn  23719  cncfmet  23760  cfilresi  24146  cfilres  24147  dvdsmulf1o  26030  sspgval  28764  sspsval  28766  sspmlem  28767  hhssabloilem  29296  hhssabloi  29297  hhssnv  29299  hhssmetdval  29312  raddcn  31547  xrge0pluscn  31558  cvmlift2lem9  32940  icoreval  35210  icoreelrnab  35211  equivbnd2  35636  ismtyres  35652  iccbnd  35684  exidreslem  35721  divrngcl  35801  isdrngo2  35802  rnghmresel  45138  rnghmsscmap2  45147  rnghmsscmap  45148  rnghmsubcsetclem2  45150  rngcifuestrc  45171  rhmresel  45184  rhmsscmap2  45193  rhmsscmap  45194  rhmsubcsetclem2  45196  rhmsscrnghm  45200  rhmsubcrngclem2  45202  rhmsubclem4  45263