Theorem ovres 7314

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ⟨cop 4573   × cxp 5553   ↾ cres 5557  ‘cfv 6355  (class class class)co 7156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-xp 5561  df-res 5567  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  ovresd  7315  oprres  7316  oprssov  7317  ofmresval  7422  cantnfval2  9132  mulnzcnopr  11286  prdsdsval3  16758  mgmsscl  17857  frmdplusg  18019  frmdadd  18020  grpissubg  18299  gaid  18429  gass  18431  gasubg  18432  mplsubrglem  20219  mamures  21001  mdetrlin  21211  mdetrsca  21212  pmatcollpw3lem  21391  tsmsxplem1  22761  tsmsxplem2  22762  xmetres2  22971  ressprdsds  22981  blres  23041  xmetresbl  23047  mscl  23071  xmscl  23072  xmsge0  23073  xmseq0  23074  nmfval2  23200  nmval2  23201  isngp3  23207  ngpds  23213  ngpocelbl  23313  xrsdsre  23418  divcn  23476  cncfmet  23516  cfilresi  23898  cfilres  23899  dvdsmulf1o  25771  sspgval  28506  sspsval  28508  sspmlem  28509  hhssabloilem  29038  hhssabloi  29039  hhssnv  29041  hhssmetdval  29054  raddcn  31172  xrge0pluscn  31183  cvmlift2lem9  32558  icoreval  34637  icoreelrnab  34638  equivbnd2  35085  ismtyres  35101  iccbnd  35133  exidreslem  35170  divrngcl  35250  isdrngo2  35251  rnghmresel  44255  rnghmsscmap2  44264  rnghmsscmap  44265  rnghmsubcsetclem2  44267  rngcifuestrc  44288  rhmresel  44301  rhmsscmap2  44310  rhmsscmap  44311  rhmsubcsetclem2  44313  rhmsscrnghm  44317  rhmsubcrngclem2  44319  rhmsubclem4  44380