![]() |
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 7288 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
6 | 1, 5 | mp3an3 1447 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 Vcvv 3441 (class class class)co 7135 ∈ cmpo 7137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 |
This theorem is referenced by: fvproj 7811 seqomlem1 8069 seqomlem4 8072 oav 8119 omv 8120 oev 8122 iunfictbso 9525 fin23lem12 9742 axdc4lem 9866 axcclem 9868 addpipq2 10347 mulpipq2 10350 subval 10866 divval 11289 cnref1o 12372 ixxval 12734 fzval 12887 modval 13234 om2uzrdg 13319 uzrdgsuci 13323 axdc4uzlem 13346 seqval 13375 seqp1 13379 bcval 13660 cnrecnv 14516 risefacval 15354 fallfacval 15355 gcdval 15835 lcmval 15926 imasvscafn 16802 imasvscaval 16803 grpsubval 18141 isghm 18350 lactghmga 18525 efgmval 18830 efgtval 18841 frgpup3lem 18895 dvrval 19431 frlmval 20437 psrvsca 20629 mat1comp 21045 mamulid 21046 mamurid 21047 madufval 21242 xkococnlem 22264 xkococn 22265 cnextval 22666 dscmet 23179 cncfval 23493 htpycom 23581 htpyid 23582 phtpycom 23593 phtpyid 23594 ehl1eudisval 24025 logbval 25352 isismt 26328 clwwlknon 27875 clwwlk0on0 27877 grpodivval 28318 ipval 28486 lnoval 28535 nmoofval 28545 bloval 28564 0ofval 28570 ajfval 28592 hvsubval 28799 hosmval 29518 hommval 29519 hodmval 29520 hfsmval 29521 hfmmval 29522 kbfval 29735 opsqrlem3 29925 dpval 30592 xdivval 30621 smatrcl 31149 smatlem 31150 mdetpmtr12 31178 pstmfval 31249 sxval 31559 ismbfm 31620 dya2iocival 31641 sitgval 31700 sitmval 31717 oddpwdcv 31723 ballotlemgval 31891 vtsval 32018 cvmlift2lem4 32666 icoreval 34770 metf1o 35193 heiborlem3 35251 heiborlem6 35254 heiborlem8 35256 heibor 35259 ldualvs 36433 tendopl 38072 cdlemkuu 38191 dvavsca 38313 dvhvaddval 38386 dvhvscaval 38395 hlhilipval 39245 resubval 39505 prjspnval 39610 rrx2xpref1o 45132 |
Copyright terms: Public domain | W3C validator |