Theorem ovres 7585

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ⟨cop 4597   × cxp 5661   ↾ cres 5665  ‘cfv 6540  (class class class)co 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-res 5675  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  ovresd  7586  oprres  7587  oprssov  7589  ofmresval  7700  cantnfval2  9645  mulnzcnf  11875  prdsdsval3  17560  mgmsscl  18725  frmdplusg  18950  frmdadd  18951  grpissubg  19257  gaid  19413  gass  19415  gasubg  19416  rnghmresel  20769  rnghmsscmap2  20778  rnghmsscmap  20779  rnghmsubcsetclem2  20781  rngcifuestrc  20788  rhmresel  20798  rhmsscmap2  20807  rhmsscmap  20808  rhmsubcsetclem2  20810  rhmsscrnghm  20814  rhmsubcrngclem2  20816  rhmsubclem4  20837  mplsubrglem  22203  mamures  22604  mdetrlin  22809  mdetrsca  22810  pmatcollpw3lem  22990  tsmsxplem1  24361  tsmsxplem2  24362  xmetres2  24569  ressprdsds  24579  blres  24639  xmetresbl  24645  mscl  24669  xmscl  24670  xmsge0  24671  xmseq0  24672  nmfval0  24798  nmval2  24800  isngp3  24806  ngpds  24812  ngpocelbl  24912  xrsdsre  25019  divcn  25078  cncfmet  25119  cfilresi  25505  cfilres  25506  mpodvdsmulf1o  27409  dvdsmulf1o  27411  zsoring  28653  sspgval  31152  sspsval  31154  sspmlem  31155  hhssabloilem  31684  hhssabloi  31685  hhssnv  31687  hhssmetdval  31700  raddcn  34383  xrge0pluscn  34394  cvmlift2lem9  35840  icoreval  38056  icoreelrnab  38057  equivbnd2  38501  ismtyres  38517  iccbnd  38549  exidreslem  38586  divrngcl  38666  isdrngo2  38667  ofoafo  44141  ofoacl  44142  naddcnfcl  44150  fuco11b  50172