Theorem dmmptg 6264

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.)

Assertion

Ref	Expression
dmmptg	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem dmmptg

Step	Hyp	Ref	Expression
1		eqid 2735	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6262	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3499	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3081	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3468	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2794	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  ∀wral 3059  {crab 3433  Vcvv 3478   ↦ cmpt 5231  dom cdm 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5695  df-rel 5696  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702

This theorem is referenced by:  rnmpt0f  6265  ovmpt3rabdm  7692  suppssov1  8221  suppssov2  8222  suppssfv  8226  iinon  8379  onoviun  8382  noinfep  9698  cantnfdm  9702  axcc2lem  10474  negfi  12215  ccatalpha  14628  swrd0  14693  o1lo1  15570  o1lo12  15571  lo1mptrcl  15655  o1mptrcl  15656  o1add2  15657  o1mul2  15658  o1sub2  15659  lo1add  15660  lo1mul  15661  o1dif  15663  rlimneg  15680  lo1le  15685  rlimno1  15687  o1fsum  15846  divsfval  17594  subdrgint  20821  iscnp2  23263  ptcnplem  23645  xkoinjcn  23711  fbasrn  23908  prdsdsf  24393  ressprdsds  24397  mbfmptcl  25685  mbfdm2  25686  dvmptresicc  25966  dvmptcl  26012  dvmptadd  26013  dvmptmul  26014  dvmptres2  26015  dvmptcmul  26017  dvmptcj  26021  dvmptco  26025  rolle  26043  dvlip  26047  dvlipcn  26048  dvle  26061  dvivthlem1  26062  dvivth  26064  dvfsumle  26075  dvfsumleOLD  26076  dvfsumge  26077  dvmptrecl  26079  dvfsumlem2  26082  dvfsumlem2OLD  26083  pserdv  26488  logtayl  26717  relogbf  26849  rlimcxp  27032  o1cxp  27033  gsummpt2co  33034  psgnfzto1stlem  33103  measdivcstALTV  34206  probfinmeasbALTV  34411  probmeasb  34412  dstrvprob  34453  cvmsss2  35259  sdclem2  37729  3factsumint1  42003  dmmzp  42721  dvcosax  45882  dvnprodlem3  45904  itgcoscmulx  45925  stoweidlem27  45983  dirkeritg  46058  fourierdlem16  46079  fourierdlem21  46084  fourierdlem22  46085  fourierdlem39  46102  fourierdlem57  46119  fourierdlem58  46120  fourierdlem60  46122  fourierdlem61  46123  fourierdlem73  46135  fourierdlem83  46145  subsaliuncllem  46313  0ome  46485  hoi2toco  46563  elbigofrcl  48400  itcoval0mpt  48516