Theorem ovres 7534

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4588   × cxp 5630   ↾ cres 5634  ‘cfv 6500  (class class class)co 7368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-res 5644  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  ovresd  7535  oprres  7536  oprssov  7537  ofmresval  7648  cantnfval2  9590  mulnzcnf  11795  prdsdsval3  17417  mgmsscl  18582  frmdplusg  18791  frmdadd  18792  grpissubg  19088  gaid  19240  gass  19242  gasubg  19243  rnghmresel  20565  rnghmsscmap2  20574  rnghmsscmap  20575  rnghmsubcsetclem2  20577  rngcifuestrc  20584  rhmresel  20594  rhmsscmap2  20603  rhmsscmap  20604  rhmsubcsetclem2  20606  rhmsscrnghm  20610  rhmsubcrngclem2  20612  rhmsubclem4  20633  mplsubrglem  21971  mamures  22353  mdetrlin  22558  mdetrsca  22559  pmatcollpw3lem  22739  tsmsxplem1  24109  tsmsxplem2  24110  xmetres2  24317  ressprdsds  24327  blres  24387  xmetresbl  24393  mscl  24417  xmscl  24418  xmsge0  24419  xmseq0  24420  nmfval0  24546  nmval2  24548  isngp3  24554  ngpds  24560  ngpocelbl  24660  xrsdsre  24767  divcnOLD  24825  divcn  24827  cncfmet  24870  cfilresi  25263  cfilres  25264  mpodvdsmulf1o  27172  dvdsmulf1o  27174  zsoring  28417  sspgval  30817  sspsval  30819  sspmlem  30820  hhssabloilem  31349  hhssabloi  31350  hhssnv  31352  hhssmetdval  31365  raddcn  34107  xrge0pluscn  34118  cvmlift2lem9  35527  icoreval  37608  icoreelrnab  37609  equivbnd2  38043  ismtyres  38059  iccbnd  38091  exidreslem  38128  divrngcl  38208  isdrngo2  38209  ofoafo  43713  ofoacl  43714  naddcnfcl  43722  fuco11b  49696