Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ovmpt2 | 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 |
---|---|
ovmpt2g.1 | ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) |
ovmpt2g.2 | ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) |
ovmpt2g.3 | ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
ovmpt2.4 | ⊢ 𝑆 ∈ V |
Ref | Expression |
---|---|
ovmpt2 | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovmpt2.4 | . 2 ⊢ 𝑆 ∈ V | |
2 | ovmpt2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) | |
3 | ovmpt2g.2 | . . 3 ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) | |
4 | ovmpt2g.3 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) | |
5 | 2, 3, 4 | ovmpt2g 6693 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
6 | 1, 5 | mp3an3 1405 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 Vcvv 3173 (class class class)co 6549 ↦ cmpt2 6551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-iota 5768 df-fun 5806 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 |
This theorem is referenced by: seqomlem1 7432 seqomlem4 7435 oav 7478 omv 7479 oev 7481 iunfictbso 8820 fin23lem12 9036 axdc4lem 9160 axcclem 9162 addpipq2 9637 mulpipq2 9640 subval 10151 divval 10566 cnref1o 11703 ixxval 12054 fzval 12199 modval 12532 om2uzrdg 12617 uzrdgsuci 12621 axdc4uzlem 12644 seqval 12674 seqp1 12678 bcval 12953 cnrecnv 13753 risefacval 14578 fallfacval 14579 gcdval 15056 lcmval 15143 imasvscafn 16020 imasvscaval 16021 grpsubval 17288 isghm 17483 lactghmga 17647 efgmval 17948 efgtval 17959 frgpup3lem 18013 dvrval 18508 psrvsca 19212 frlmval 19911 mat1comp 20065 mamulid 20066 mamurid 20067 madufval 20262 xkococnlem 21272 xkococn 21273 cnextval 21675 dscmet 22187 cncfval 22499 htpycom 22583 htpyid 22584 phtpycom 22595 phtpyid 22596 logbval 24304 isismt 25229 grpodivval 26773 ipval 26942 lnoval 26991 nmoofval 27001 bloval 27020 0ofval 27026 ajfval 27048 hvsubval 27257 hosmval 27978 hommval 27979 hodmval 27980 hfsmval 27981 hfmmval 27982 kbfval 28195 opsqrlem3 28385 xdivval 28958 smatrcl 29190 smatlem 29191 mdetpmtr12 29219 fvproj 29227 pstmfval 29267 sxval 29580 ismbfm 29641 dya2iocival 29662 sitgval 29721 sitmval 29738 oddpwdcv 29744 ballotlemgval 29912 cvmlift2lem4 30542 icoreval 32377 metf1o 32721 heiborlem3 32782 heiborlem6 32785 heiborlem8 32787 heibor 32790 ldualvs 33442 tendopl 35082 cdlemkuu 35201 dvavsca 35323 dvhvaddval 35397 dvhvscaval 35406 hlhilipval 36259 wwlks2onv 41158 dpval 42310 |
Copyright terms: Public domain | W3C validator |