Theorem ovres 7515

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4583   × cxp 5617   ↾ cres 5621  ‘cfv 6482  (class class class)co 7349

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-res 5631  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  ovresd  7516  oprres  7517  oprssov  7518  ofmresval  7629  cantnfval2  9565  mulnzcnf  11766  prdsdsval3  17389  mgmsscl  18519  frmdplusg  18728  frmdadd  18729  grpissubg  19025  gaid  19178  gass  19180  gasubg  19181  rnghmresel  20505  rnghmsscmap2  20514  rnghmsscmap  20515  rnghmsubcsetclem2  20517  rngcifuestrc  20524  rhmresel  20534  rhmsscmap2  20543  rhmsscmap  20544  rhmsubcsetclem2  20546  rhmsscrnghm  20550  rhmsubcrngclem2  20552  rhmsubclem4  20573  mplsubrglem  21911  mamures  22282  mdetrlin  22487  mdetrsca  22488  pmatcollpw3lem  22668  tsmsxplem1  24038  tsmsxplem2  24039  xmetres2  24247  ressprdsds  24257  blres  24317  xmetresbl  24323  mscl  24347  xmscl  24348  xmsge0  24349  xmseq0  24350  nmfval0  24476  nmval2  24478  isngp3  24484  ngpds  24490  ngpocelbl  24590  xrsdsre  24697  divcnOLD  24755  divcn  24757  cncfmet  24800  cfilresi  25193  cfilres  25194  mpodvdsmulf1o  27102  dvdsmulf1o  27104  zsoring  28301  sspgval  30673  sspsval  30675  sspmlem  30676  hhssabloilem  31205  hhssabloi  31206  hhssnv  31208  hhssmetdval  31221  raddcn  33896  xrge0pluscn  33907  cvmlift2lem9  35284  icoreval  37327  icoreelrnab  37328  equivbnd2  37772  ismtyres  37788  iccbnd  37820  exidreslem  37857  divrngcl  37937  isdrngo2  37938  ofoafo  43329  ofoacl  43330  naddcnfcl  43338  fuco11b  49322