![]() |
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 6837 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
6 | 1, 5 | mp3an3 1453 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1523 ∈ wcel 2030 Vcvv 3231 (class class class)co 6690 ↦ cmpt2 6692 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-opab 4746 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-iota 5889 df-fun 5928 df-fv 5934 df-ov 6693 df-oprab 6694 df-mpt2 6695 |
This theorem is referenced by: seqomlem1 7590 seqomlem4 7593 oav 7636 omv 7637 oev 7639 iunfictbso 8975 fin23lem12 9191 axdc4lem 9315 axcclem 9317 addpipq2 9796 mulpipq2 9799 subval 10310 divval 10725 cnref1o 11865 ixxval 12221 fzval 12366 modval 12710 om2uzrdg 12795 uzrdgsuci 12799 axdc4uzlem 12822 seqval 12852 seqp1 12856 bcval 13131 cnrecnv 13949 risefacval 14783 fallfacval 14784 gcdval 15265 lcmval 15352 imasvscafn 16244 imasvscaval 16245 grpsubval 17512 isghm 17707 lactghmga 17870 efgmval 18171 efgtval 18182 frgpup3lem 18236 dvrval 18731 psrvsca 19439 frlmval 20140 mat1comp 20294 mamulid 20295 mamurid 20296 madufval 20491 xkococnlem 21510 xkococn 21511 cnextval 21912 dscmet 22424 cncfval 22738 htpycom 22822 htpyid 22823 phtpycom 22834 phtpyid 22835 logbval 24549 isismt 25474 clwwlknon 27063 clwwlknonOLD 27064 clwwlk0on0 27067 grpodivval 27517 ipval 27686 lnoval 27735 nmoofval 27745 bloval 27764 0ofval 27770 ajfval 27792 hvsubval 28001 hosmval 28722 hommval 28723 hodmval 28724 hfsmval 28725 hfmmval 28726 kbfval 28939 opsqrlem3 29129 dpval 29725 xdivval 29755 smatrcl 29990 smatlem 29991 mdetpmtr12 30019 fvproj 30027 pstmfval 30067 sxval 30381 ismbfm 30442 dya2iocival 30463 sitgval 30522 sitmval 30539 oddpwdcv 30545 ballotlemgval 30713 vtsval 30843 cvmlift2lem4 31414 icoreval 33331 metf1o 33681 heiborlem3 33742 heiborlem6 33745 heiborlem8 33747 heibor 33750 ldualvs 34742 tendopl 36381 cdlemkuu 36500 dvavsca 36622 dvhvaddval 36696 dvhvscaval 36705 hlhilipval 37558 |
Copyright terms: Public domain | W3C validator |