Theorem ovres 7558

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4598   × cxp 5639   ↾ cres 5643  ‘cfv 6514  (class class class)co 7390

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-res 5653  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  ovresd  7559  oprres  7560  oprssov  7561  ofmresval  7672  cantnfval2  9629  mulnzcnf  11831  prdsdsval3  17455  mgmsscl  18579  frmdplusg  18788  frmdadd  18789  grpissubg  19085  gaid  19238  gass  19240  gasubg  19241  rnghmresel  20536  rnghmsscmap2  20545  rnghmsscmap  20546  rnghmsubcsetclem2  20548  rngcifuestrc  20555  rhmresel  20565  rhmsscmap2  20574  rhmsscmap  20575  rhmsubcsetclem2  20577  rhmsscrnghm  20581  rhmsubcrngclem2  20583  rhmsubclem4  20604  mplsubrglem  21920  mamures  22291  mdetrlin  22496  mdetrsca  22497  pmatcollpw3lem  22677  tsmsxplem1  24047  tsmsxplem2  24048  xmetres2  24256  ressprdsds  24266  blres  24326  xmetresbl  24332  mscl  24356  xmscl  24357  xmsge0  24358  xmseq0  24359  nmfval0  24485  nmval2  24487  isngp3  24493  ngpds  24499  ngpocelbl  24599  xrsdsre  24706  divcnOLD  24764  divcn  24766  cncfmet  24809  cfilresi  25202  cfilres  25203  mpodvdsmulf1o  27111  dvdsmulf1o  27113  sspgval  30665  sspsval  30667  sspmlem  30668  hhssabloilem  31197  hhssabloi  31198  hhssnv  31200  hhssmetdval  31213  raddcn  33926  xrge0pluscn  33937  cvmlift2lem9  35305  icoreval  37348  icoreelrnab  37349  equivbnd2  37793  ismtyres  37809  iccbnd  37841  exidreslem  37878  divrngcl  37958  isdrngo2  37959  ofoafo  43352  ofoacl  43353  naddcnfcl  43361  fuco11b  49330