![]() |
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 5715 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
2 | 1 | fvresd 6916 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘〈𝐴, 𝐵〉) = (𝐹‘〈𝐴, 𝐵〉)) |
3 | df-ov 7422 | . 2 ⊢ (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = ((𝐹 ↾ (𝐶 × 𝐷))‘〈𝐴, 𝐵〉) | |
4 | df-ov 7422 | . 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
5 | 2, 3, 4 | 3eqtr4g 2790 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 〈cop 4636 × cxp 5676 ↾ cres 5680 ‘cfv 6549 (class class class)co 7419 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-xp 5684 df-res 5690 df-iota 6501 df-fv 6557 df-ov 7422 |
This theorem is referenced by: ovresd 7588 oprres 7589 oprssov 7590 ofmresval 7701 cantnfval2 9694 mulnzcnf 11892 prdsdsval3 17470 mgmsscl 18608 frmdplusg 18814 frmdadd 18815 grpissubg 19109 gaid 19262 gass 19264 gasubg 19265 rnghmresel 20565 rnghmsscmap2 20574 rnghmsscmap 20575 rnghmsubcsetclem2 20577 rngcifuestrc 20584 rhmresel 20594 rhmsscmap2 20603 rhmsscmap 20604 rhmsubcsetclem2 20606 rhmsscrnghm 20610 rhmsubcrngclem2 20612 rhmsubclem4 20633 mplsubrglem 21966 mamures 22341 mdetrlin 22548 mdetrsca 22549 pmatcollpw3lem 22729 tsmsxplem1 24101 tsmsxplem2 24102 xmetres2 24311 ressprdsds 24321 blres 24381 xmetresbl 24387 mscl 24411 xmscl 24412 xmsge0 24413 xmseq0 24414 nmfval0 24543 nmval2 24545 isngp3 24551 ngpds 24557 ngpocelbl 24665 xrsdsre 24770 divcnOLD 24828 divcn 24830 cncfmet 24873 cfilresi 25267 cfilres 25268 mpodvdsmulf1o 27171 dvdsmulf1o 27173 sspgval 30611 sspsval 30613 sspmlem 30614 hhssabloilem 31143 hhssabloi 31144 hhssnv 31146 hhssmetdval 31159 raddcn 33661 xrge0pluscn 33672 cvmlift2lem9 35052 icoreval 36963 icoreelrnab 36964 equivbnd2 37396 ismtyres 37412 iccbnd 37444 exidreslem 37481 divrngcl 37561 isdrngo2 37562 ofoafo 42927 ofoacl 42928 naddcnfcl 42936 |
Copyright terms: Public domain | W3C validator |