Theorem ovres 7584

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ⟨cop 4590   × cxp 5649   ↾ cres 5653  ‘cfv 6537  (class class class)co 7418

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-res 5663  df-iota 6493  df-fv 6545  df-ov 7421

This theorem is used by:  ovresd  7585  oprres  7586  oprssov  7588  ofmresval  7707  cantnfval2  9663  mulnzcnf  11955  prdsdsval3  17649  mgmsscl  18814  frmdplusg  19043  frmdadd  19044  grpissubg  19350  gaid  19506  gass  19508  gasubg  19509  rnghmresel  20865  rnghmsscmap2  20874  rnghmsscmap  20875  rnghmsubcsetclem2  20877  rngcifuestrc  20884  rhmresel  20894  rhmsscmap2  20903  rhmsscmap  20904  rhmsubcsetclem2  20906  rhmsscrnghm  20910  rhmsubcrngclem2  20912  rhmsubclem4  20933  mplsubrglem  22304  mamures  22705  mdetrlin  22910  mdetrsca  22911  pmatcollpw3lem  23094  tsmsxplem1  24465  tsmsxplem2  24466  xmetres2  24673  ressprdsds  24683  blres  24743  xmetresbl  24749  mscl  24773  xmscl  24774  xmsge0  24775  xmseq0  24776  nmfval0  24902  nmval2  24904  isngp3  24910  ngpds  24916  ngpocelbl  25016  xrsdsre  25123  divcn  25182  cncfmet  25223  cfilresi  25609  cfilres  25610  mpodvdsmulf1o  27514  dvdsmulf1o  27516  zsoring  28788  sspgval  31324  sspsval  31326  sspmlem  31327  hhssabloilem  31856  hhssabloi  31857  hhssnv  31859  hhssmetdval  31872  raddcn  34554  xrge0pluscn  34565  cvmlift2lem9  36055  icoreval  38256  icoreelrnab  38257  equivbnd2  38706  ismtyres  38722  iccbnd  38754  exidreslem  38791  divrngcl  38871  isdrngo2  38872  ofoafo  44342  ofoacl  44343  naddcnfcl  44351  fuco11b  50414