Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ovmpo | Structured version Visualization version GIF version |
Description: Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
Ref | Expression |
---|---|
ovmpog.1 | ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) |
ovmpog.2 | ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) |
ovmpog.3 | ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
ovmpo.4 | ⊢ 𝑆 ∈ V |
Ref | Expression |
---|---|
ovmpo | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovmpo.4 | . 2 ⊢ 𝑆 ∈ V | |
2 | ovmpog.1 | . . 3 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) | |
3 | ovmpog.2 | . . 3 ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) | |
4 | ovmpog.3 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) | |
5 | 2, 3, 4 | ovmpog 7386 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
6 | 1, 5 | mp3an3 1452 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2111 Vcvv 3420 (class class class)co 7231 ∈ cmpo 7233 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-sep 5206 ax-nul 5213 ax-pr 5336 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ral 3067 df-rex 3068 df-rab 3071 df-v 3422 df-sbc 3709 df-dif 3883 df-un 3885 df-in 3887 df-ss 3897 df-nul 4252 df-if 4454 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4834 df-br 5068 df-opab 5130 df-id 5469 df-xp 5571 df-rel 5572 df-cnv 5573 df-co 5574 df-dm 5575 df-iota 6355 df-fun 6399 df-fv 6405 df-ov 7234 df-oprab 7235 df-mpo 7236 |
This theorem is referenced by: fvproj 7921 seqomlem1 8206 seqomlem4 8209 oav 8258 omv 8259 oev 8261 iunfictbso 9752 fin23lem12 9969 axdc4lem 10093 axcclem 10095 addpipq2 10574 mulpipq2 10577 subval 11093 divval 11516 cnref1o 12605 ixxval 12967 fzval 13121 modval 13468 om2uzrdg 13553 uzrdgsuci 13557 axdc4uzlem 13580 seqval 13609 seqp1 13613 bcval 13894 cnrecnv 14752 risefacval 15594 fallfacval 15595 gcdval 16079 lcmval 16173 imasvscafn 17066 imasvscaval 17067 grpsubval 18437 isghm 18646 lactghmga 18821 efgmval 19126 efgtval 19137 frgpup3lem 19191 dvrval 19727 frlmval 20734 psrvsca 20940 mat1comp 21361 mamulid 21362 mamurid 21363 madufval 21558 xkococnlem 22580 xkococn 22581 cnextval 22982 dscmet 23494 cncfval 23809 htpycom 23897 htpyid 23898 phtpycom 23909 phtpyid 23910 ehl1eudisval 24342 logbval 25673 isismt 26649 clwwlknon 28197 clwwlk0on0 28199 grpodivval 28640 ipval 28808 lnoval 28857 nmoofval 28867 bloval 28886 0ofval 28892 ajfval 28914 hvsubval 29121 hosmval 29840 hommval 29841 hodmval 29842 hfsmval 29843 hfmmval 29844 kbfval 30057 opsqrlem3 30247 dpval 30908 xdivval 30937 smatrcl 31484 smatlem 31485 mdetpmtr12 31513 pstmfval 31584 sxval 31894 ismbfm 31955 dya2iocival 31976 sitgval 32035 sitmval 32052 oddpwdcv 32058 ballotlemgval 32226 vtsval 32353 cvmlift2lem4 33004 addsval 33889 icoreval 35287 metf1o 35676 heiborlem3 35734 heiborlem6 35737 heiborlem8 35739 heibor 35742 ldualvs 36914 tendopl 38553 cdlemkuu 38672 dvavsca 38794 dvhvaddval 38867 dvhvscaval 38876 hlhilipval 39726 resubval 40086 prjspnval 40191 rrx2xpref1o 45765 functhinclem1 46023 |
Copyright terms: Public domain | W3C validator |