![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmmptg | Structured version Visualization version GIF version |
Description: The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.) |
Ref | Expression |
---|---|
dmmptg | ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2725 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | 1 | dmmpt 6246 | . 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
3 | elex 3480 | . . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) | |
4 | 3 | ralimi 3072 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
5 | rabid2 3452 | . . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) | |
6 | 4, 5 | sylibr 233 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}) |
7 | 2, 6 | eqtr4id 2784 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ∀wral 3050 {crab 3418 Vcvv 3461 ↦ cmpt 5232 dom cdm 5678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-mpt 5233 df-xp 5684 df-rel 5685 df-cnv 5686 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 |
This theorem is referenced by: rnmpt0f 6249 ovmpt3rabdm 7680 suppssov1 8203 suppssov2 8204 suppssfv 8208 iinon 8361 onoviun 8364 noinfep 9690 cantnfdm 9694 axcc2lem 10466 negfi 12201 ccatalpha 14584 swrd0 14649 o1lo1 15522 o1lo12 15523 lo1mptrcl 15607 o1mptrcl 15608 o1add2 15609 o1mul2 15610 o1sub2 15611 lo1add 15612 lo1mul 15613 o1dif 15615 rlimneg 15634 lo1le 15639 rlimno1 15641 o1fsum 15800 divsfval 17537 subdrgint 20708 iscnp2 23192 ptcnplem 23574 xkoinjcn 23640 fbasrn 23837 prdsdsf 24322 ressprdsds 24326 mbfmptcl 25614 mbfdm2 25615 dvmptresicc 25894 dvmptcl 25940 dvmptadd 25941 dvmptmul 25942 dvmptres2 25943 dvmptcmul 25945 dvmptcj 25949 dvmptco 25953 rolle 25971 dvlip 25975 dvlipcn 25976 dvle 25989 dvivthlem1 25990 dvivth 25992 dvfsumle 26003 dvfsumleOLD 26004 dvfsumge 26005 dvmptrecl 26007 dvfsumlem2 26010 dvfsumlem2OLD 26011 pserdv 26416 logtayl 26644 relogbf 26773 rlimcxp 26956 o1cxp 26957 gsummpt2co 32857 psgnfzto1stlem 32918 measdivcstALTV 33977 probfinmeasbALTV 34182 probmeasb 34183 dstrvprob 34224 cvmsss2 35017 sdclem2 37348 3factsumint1 41626 dmmzp 42297 dvcosax 45454 dvnprodlem3 45476 itgcoscmulx 45497 stoweidlem27 45555 dirkeritg 45630 fourierdlem16 45651 fourierdlem21 45656 fourierdlem22 45657 fourierdlem39 45674 fourierdlem57 45691 fourierdlem58 45692 fourierdlem60 45694 fourierdlem61 45695 fourierdlem73 45707 fourierdlem83 45717 subsaliuncllem 45885 0ome 46057 hoi2toco 46135 elbigofrcl 47811 itcoval0mpt 47927 |
Copyright terms: Public domain | W3C validator |