| 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 7592 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
| 6 | 1, 5 | mp3an3 1452 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 Vcvv 3480 (class class class)co 7431 ∈ cmpo 7433 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-iota 6514 df-fun 6563 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 |
| This theorem is referenced by: fvproj 8159 seqomlem1 8490 seqomlem4 8493 oav 8549 omv 8550 oev 8552 iunfictbso 10154 fin23lem12 10371 axdc4lem 10495 axcclem 10497 addpipq2 10976 mulpipq2 10979 subval 11499 divval 11924 cnref1o 13027 ixxval 13395 fzval 13549 modval 13911 om2uzrdg 13997 uzrdgsuci 14001 axdc4uzlem 14024 seqval 14053 seqp1 14057 bcval 14343 cnrecnv 15204 risefacval 16044 fallfacval 16045 gcdval 16533 lcmval 16629 imasvscafn 17582 imasvscaval 17583 grpsubval 19003 isghmOLD 19234 lactghmga 19423 efgmval 19730 efgtval 19741 frgpup3lem 19795 dvrval 20403 frlmval 21768 psrvsca 21969 mat1comp 22446 mamulid 22447 mamurid 22448 madufval 22643 xkococnlem 23667 xkococn 23668 cnextval 24069 dscmet 24585 cncfval 24914 htpycom 25008 htpyid 25009 phtpycom 25020 phtpyid 25021 ehl1eudisval 25455 logbval 26809 addsval 27995 subsval 28090 mulsval 28135 divsval 28215 seqsval 28294 om2noseqrdg 28310 noseqrdgsuc 28314 seqsp1 28317 expsval 28408 isismt 28542 clwwlknon 30109 clwwlk0on0 30111 grpodivval 30554 ipval 30722 lnoval 30771 nmoofval 30781 bloval 30800 0ofval 30806 ajfval 30828 hvsubval 31035 hosmval 31754 hommval 31755 hodmval 31756 hfsmval 31757 hfmmval 31758 kbfval 31971 opsqrlem3 32161 dpval 32872 xdivval 32901 smatrcl 33795 smatlem 33796 mdetpmtr12 33824 pstmfval 33895 sxval 34191 ismbfm 34252 dya2iocival 34275 sitgval 34334 sitmval 34351 oddpwdcv 34357 ballotlemgval 34526 vtsval 34652 cvmlift2lem4 35311 icoreval 37354 metf1o 37762 heiborlem3 37820 heiborlem6 37823 heiborlem8 37825 heibor 37828 ldualvs 39138 tendopl 40778 cdlemkuu 40897 dvavsca 41019 dvhvaddval 41092 dvhvscaval 41101 hlhilipval 41955 resubval 42397 prjspnval 42626 rrx2xpref1o 48639 fuco22natlem 49040 functhinclem1 49093 |
| Copyright terms: Public domain | W3C validator |