![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovres | Structured version Visualization version GIF version |
Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006.) |
Ref | Expression |
---|---|
ovres | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxpi 5444 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
2 | 1 | fvresd 6519 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘〈𝐴, 𝐵〉) = (𝐹‘〈𝐴, 𝐵〉)) |
3 | df-ov 6979 | . 2 ⊢ (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = ((𝐹 ↾ (𝐶 × 𝐷))‘〈𝐴, 𝐵〉) | |
4 | df-ov 6979 | . 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
5 | 2, 3, 4 | 3eqtr4g 2839 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 〈cop 4447 × cxp 5405 ↾ cres 5409 ‘cfv 6188 (class class class)co 6976 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-xp 5413 df-res 5419 df-iota 6152 df-fv 6196 df-ov 6979 |
This theorem is referenced by: ovresd 7131 oprres 7132 oprssov 7133 ofmresval 7240 cantnfval2 8926 mulnzcnopr 11087 prdsdsval3 16614 frmdplusg 17860 frmdadd 17861 grpissubg 18083 gaid 18200 gass 18202 gasubg 18203 mplsubrglem 19933 mamures 20703 mdetrlin 20915 mdetrsca 20916 pmatcollpw3lem 21095 tsmsxplem1 22464 tsmsxplem2 22465 xmetres2 22674 ressprdsds 22684 blres 22744 xmetresbl 22750 mscl 22774 xmscl 22775 xmsge0 22776 xmseq0 22777 nmfval2 22903 nmval2 22904 isngp3 22910 ngpds 22916 ngpocelbl 23016 xrsdsre 23121 divcn 23179 cncfmet 23219 cfilresi 23601 cfilres 23602 dvdsmulf1o 25473 sspgval 28283 sspsval 28285 sspmlem 28286 hhssabloilem 28817 hhssabloi 28818 hhssnv 28820 hhssmetdval 28834 raddcn 30822 xrge0pluscn 30833 cvmlift2lem9 32149 icoreval 34082 icoreelrnab 34083 equivbnd2 34518 ismtyres 34534 iccbnd 34566 exidreslem 34603 divrngcl 34683 isdrngo2 34684 rnghmresel 43605 rnghmsscmap2 43614 rnghmsscmap 43615 rnghmsubcsetclem2 43617 rngcifuestrc 43638 rhmresel 43651 rhmsscmap2 43660 rhmsscmap 43661 rhmsubcsetclem2 43663 rhmsscrnghm 43667 rhmsubcrngclem2 43669 rhmsubclem4 43730 |
Copyright terms: Public domain | W3C validator |