![]() |
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 7565 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆) |
5 | 1, 4 | mp3an3 1449 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2105 Vcvv 3473 (class class class)co 7412 ∈ cmpo 7414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-sbc 3778 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-iota 6495 df-fun 6545 df-fv 6551 df-ov 7415 df-oprab 7416 df-mpo 7417 |
This theorem is referenced by: ovmpot 7572 1st2val 8007 2nd2val 8008 mptmpoopabbrd 8071 mptmpoopabbrdOLD 8072 cantnffval 9664 cantnfsuc 9671 fseqenlem1 10025 xaddval 13209 xmulval 13211 fzoval 13640 expval 14036 ccatfval 14530 splcl 14709 cshfn 14747 bpolylem 15999 ruclem1 16181 sadfval 16400 sadcp1 16403 smufval 16425 smupp1 16428 eucalgval2 16525 pcval 16784 pc0 16794 vdwapval 16913 pwsval 17439 xpsfval 17519 xpsval 17523 rescval 17781 isfunc 17821 isfull 17870 isfth 17874 natfval 17907 catcisolem 18070 xpchom 18142 1stfval 18153 2ndfval 18156 yonedalem3a 18237 yonedainv 18244 plusfval 18578 ismgmhm 18627 ismhm 18713 mulgval 18997 eqgfval 19099 isga 19203 subgga 19212 cayleylem1 19328 sylow1lem2 19515 isslw 19524 sylow2blem1 19536 sylow3lem1 19543 sylow3lem6 19548 frgpuptinv 19687 frgpup2 19692 isrhm 20376 scafval 20723 islmhm 20871 xrsdsval 21278 ipfval 21512 dsmmval 21599 psrmulfval 21815 mplval 21859 ltbval 21909 mpfrcl 21959 evlsval 21960 evlval 21969 mhpfval 21991 matval 22231 submafval 22401 mdetfval 22408 minmar1fval 22468 txval 23388 xkoval 23411 hmeofval 23582 flffval 23813 qustgplem 23945 dscmet 24401 dscopn 24402 tngval 24468 nmofval 24551 nghmfval 24559 isnmhm 24583 htpyco1 24824 htpycc 24826 phtpycc 24837 reparphti 24843 reparphtiOLD 24844 pcoval 24858 pcohtpylem 24866 pcorevlem 24873 dyadval 25441 itg1addlem3 25547 itg1addlem4 25548 itg1addlem4OLD 25549 mbfi1fseqlem3 25567 mbfi1fseqlem4 25568 mbfi1fseqlem5 25569 mbfi1fseqlem6 25570 mdegfval 25918 quotval 26144 elqaalem2 26172 cxpval 26512 cxpcn3 26597 angval 26647 sgmval 26987 lgsval 27147 wwlksn 29524 wspthsn 29535 rusgrnumwwlklem 29657 clwwlkn 29712 2clwwlk 30033 numclwwlkovh0 30058 numclwwlkovq 30060 shsval 30998 sshjval 31036 faeval 33708 txsconnlem 34695 cvxsconn 34698 iscvm 34714 cvmliftlem5 34744 mpomulnzcnf 35629 rngohomval 37296 rngoisoval 37309 evlselv 41622 prjcrvfval 41836 rmxfval 42105 rmyfval 42106 mendplusg 42391 mendvsca 42396 mnringvald 43430 addrval 43688 subrval 43689 mulvval 43690 sigarval 46025 dmatALTval 47243 naryfval 47476 |
Copyright terms: Public domain | W3C validator |