![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovmpoa | Structured version Visualization version GIF version |
Description: Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.) |
Ref | Expression |
---|---|
ovmpoga.1 | ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) |
ovmpoga.2 | ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
ovmpoa.4 | ⊢ 𝑆 ∈ V |
Ref | Expression |
---|---|
ovmpoa | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovmpoa.4 | . 2 ⊢ 𝑆 ∈ V | |
2 | ovmpoga.1 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) | |
3 | ovmpoga.2 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) | |
4 | 2, 3 | ovmpoga 7160 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
5 | 1, 4 | mp3an3 1442 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2081 Vcvv 3437 (class class class)co 7016 ∈ cmpo 7018 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-iota 6189 df-fun 6227 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 |
This theorem is referenced by: 1st2val 7573 2nd2val 7574 cantnffval 8972 cantnfsuc 8979 fseqenlem1 9296 xaddval 12466 xmulval 12468 fzoval 12889 expval 13281 ccatfval 13771 splcl 13950 cshfn 13988 bpolylem 15235 ruclem1 15417 sadfval 15634 sadcp1 15637 smufval 15659 smupp1 15662 eucalgval2 15754 pcval 16010 pc0 16020 vdwapval 16138 pwsval 16588 xpsfval 16668 xpsval 16672 rescval 16926 isfunc 16963 isfull 17009 isfth 17013 natfval 17045 catcisolem 17195 xpchom 17259 1stfval 17270 2ndfval 17273 yonedalem3a 17353 yonedainv 17360 plusfval 17687 ismhm 17776 mulgval 17985 eqgfval 18081 isga 18162 subgga 18171 cayleylem1 18271 sylow1lem2 18454 isslw 18463 sylow2blem1 18475 sylow3lem1 18482 sylow3lem6 18487 frgpuptinv 18624 frgpup2 18629 isrhm 19163 scafval 19343 islmhm 19489 psrmulfval 19853 mplval 19896 ltbval 19939 mpfrcl 19985 evlsval 19986 evlval 19991 xrsdsval 20271 ipfval 20475 dsmmval 20560 matval 20704 submafval 20872 mdetfval 20879 minmar1fval 20939 txval 21856 xkoval 21879 hmeofval 22050 flffval 22281 qustgplem 22412 dscmet 22865 dscopn 22866 tngval 22931 nmofval 23006 nghmfval 23014 isnmhm 23038 htpyco1 23265 htpycc 23267 phtpycc 23278 reparphti 23284 pcoval 23298 pcohtpylem 23306 pcorevlem 23313 dyadval 23876 itg1addlem3 23982 itg1addlem4 23983 mbfi1fseqlem3 24001 mbfi1fseqlem4 24002 mbfi1fseqlem5 24003 mbfi1fseqlem6 24004 mdegfval 24339 quotval 24564 elqaalem2 24592 cxpval 24928 cxpcn3 25010 angval 25060 sgmval 25401 lgsval 25559 wwlksn 27302 wspthsn 27313 rusgrnumwwlklem 27436 clwwlkn 27491 2clwwlk 27818 numclwwlkovh0 27843 numclwwlkovq 27845 shsval 28780 sshjval 28818 faeval 31122 txsconnlem 32095 cvxsconn 32098 iscvm 32114 cvmliftlem5 32144 rngohomval 34774 rngoisoval 34787 rmxfval 38986 rmyfval 38987 mendplusg 39271 mendvsca 39276 addrval 40337 subrval 40338 mulvval 40339 sigarval 42649 ismgmhm 43532 dmatALTval 43935 |
Copyright terms: Public domain | W3C validator |