| 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 7587 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
| 5 | 1, 4 | 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: ovmpot 7594 1st2val 8042 2nd2val 8043 mptmpoopabbrd 8105 mptmpoopabbrdOLD 8106 cantnffval 9703 cantnfsuc 9710 fseqenlem1 10064 xaddval 13265 xmulval 13267 fzoval 13700 expval 14104 ccatfval 14611 splcl 14790 cshfn 14828 bpolylem 16084 ruclem1 16267 sadfval 16489 sadcp1 16492 smufval 16514 smupp1 16517 eucalgval2 16618 pcval 16882 pc0 16892 vdwapval 17011 pwsval 17531 xpsfval 17611 xpsval 17615 rescval 17871 isfunc 17909 isfull 17957 isfth 17961 natfval 17994 catcisolem 18155 xpchom 18225 1stfval 18236 2ndfval 18239 yonedalem3a 18319 yonedainv 18326 plusfval 18660 ismgmhm 18709 ismhm 18798 mulgval 19089 eqgfval 19194 isghm 19233 isga 19309 subgga 19318 cayleylem1 19430 sylow1lem2 19617 isslw 19626 sylow2blem1 19638 sylow3lem1 19645 sylow3lem6 19650 frgpuptinv 19789 frgpup2 19794 isrhm 20478 scafval 20879 islmhm 21026 xrsdsval 21428 ipfval 21667 dsmmval 21754 psrmulfval 21963 mplval 22009 ltbval 22061 mpfrcl 22109 evlsval 22110 evlval 22119 mhpfval 22142 matval 22415 submafval 22585 mdetfval 22592 minmar1fval 22652 txval 23572 xkoval 23595 hmeofval 23766 flffval 23997 qustgplem 24129 dscmet 24585 dscopn 24586 tngval 24652 nmofval 24735 nghmfval 24743 isnmhm 24767 htpyco1 25010 htpycc 25012 phtpycc 25023 reparphti 25029 reparphtiOLD 25030 pcoval 25044 pcohtpylem 25052 pcorevlem 25059 dyadval 25627 itg1addlem3 25733 itg1addlem4 25734 mbfi1fseqlem3 25752 mbfi1fseqlem4 25753 mbfi1fseqlem5 25754 mbfi1fseqlem6 25755 mdegfval 26101 quotval 26334 elqaalem2 26362 cxpval 26706 cxpcn3 26791 angval 26844 sgmval 27185 lgsval 27345 wwlksn 29857 wspthsn 29868 rusgrnumwwlklem 29990 clwwlkn 30045 2clwwlk 30366 numclwwlkovh0 30391 numclwwlkovq 30393 shsval 31331 sshjval 31369 faeval 34247 txsconnlem 35245 cvxsconn 35248 iscvm 35264 cvmliftlem5 35294 mpomulnzcnf 36300 rngohomval 37971 rngoisoval 37984 evlselv 42597 prjcrvfval 42641 rmxfval 42915 rmyfval 42916 mendplusg 43194 mendvsca 43199 mnringvald 44227 addrval 44485 subrval 44486 mulvval 44487 sigarval 46865 dmatALTval 48317 naryfval 48549 upfval 48933 |
| Copyright terms: Public domain | W3C validator |