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 | elex 3185 | . . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) | |
2 | 1 | ralimi 2936 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
3 | rabid2 3096 | . . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) | |
4 | 2, 3 | sylibr 223 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}) |
5 | eqid 2610 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
6 | 5 | dmmpt 5547 | . 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
7 | 4, 6 | syl6reqr 2663 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ∀wral 2896 {crab 2900 Vcvv 3173 ↦ cmpt 4643 dom cdm 5038 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-mpt 4645 df-xp 5044 df-rel 5045 df-cnv 5046 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 |
This theorem is referenced by: ovmpt3rabdm 6790 suppssov1 7214 suppssfv 7218 iinon 7324 onoviun 7327 noinfep 8440 cantnfdm 8444 axcc2lem 9141 negfi 10850 ccatalpha 13228 swrd0 13286 o1lo1 14116 o1lo12 14117 lo1mptrcl 14200 o1mptrcl 14201 o1add2 14202 o1mul2 14203 o1sub2 14204 lo1add 14205 lo1mul 14206 o1dif 14208 rlimneg 14225 lo1le 14230 rlimno1 14232 o1fsum 14386 divsfval 16030 iscnp2 20853 ptcnplem 21234 xkoinjcn 21300 fbasrn 21498 prdsdsf 21982 ressprdsds 21986 mbfmptcl 23210 mbfdm2 23211 dvmptcl 23528 dvmptadd 23529 dvmptmul 23530 dvmptres2 23531 dvmptcmul 23533 dvmptcj 23537 dvmptco 23541 rolle 23557 dvlip 23560 dvlipcn 23561 dvle 23574 dvivthlem1 23575 dvivth 23577 dvfsumle 23588 dvfsumge 23589 dvmptrecl 23591 dvfsumlem2 23594 pserdv 23987 logtayl 24206 relogbf 24329 rlimcxp 24500 o1cxp 24501 gsummpt2co 29111 psgnfzto1stlem 29181 measdivcstOLD 29614 probfinmeasbOLD 29817 probmeasb 29819 dstrvprob 29860 cvmsss2 30510 sdclem2 32708 dmmzp 36314 rnmpt0 38407 dvmptresicc 38809 dvcosax 38816 dvnprodlem3 38838 itgcoscmulx 38861 stoweidlem27 38920 dirkeritg 38995 fourierdlem16 39016 fourierdlem21 39021 fourierdlem22 39022 fourierdlem39 39039 fourierdlem57 39056 fourierdlem58 39057 fourierdlem60 39059 fourierdlem61 39060 fourierdlem73 39072 fourierdlem83 39082 subsaliuncllem 39251 0ome 39419 hoi2toco 39497 elbigofrcl 42142 |
Copyright terms: Public domain | W3C validator |