Theorem dmmptg 6160

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 2736	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6158	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3455	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3326	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 233	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2795	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ∀wral 3062  {crab 3284  Vcvv 3437   ↦ cmpt 5164  dom cdm 5600

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-mpt 5165  df-xp 5606  df-rel 5607  df-cnv 5608  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613

This theorem is referenced by:  rnmpt0f  6161  ovmpt3rabdm  7560  suppssov1  8045  suppssfv  8049  iinon  8202  onoviun  8205  noinfep  9462  cantnfdm  9466  axcc2lem  10238  negfi  11970  ccatalpha  14343  swrd0  14416  o1lo1  15291  o1lo12  15292  lo1mptrcl  15376  o1mptrcl  15377  o1add2  15378  o1mul2  15379  o1sub2  15380  lo1add  15381  lo1mul  15382  o1dif  15384  rlimneg  15403  lo1le  15408  rlimno1  15410  o1fsum  15570  divsfval  17303  subdrgint  20116  iscnp2  22435  ptcnplem  22817  xkoinjcn  22883  fbasrn  23080  prdsdsf  23565  ressprdsds  23569  mbfmptcl  24845  mbfdm2  24846  dvmptresicc  25125  dvmptcl  25168  dvmptadd  25169  dvmptmul  25170  dvmptres2  25171  dvmptcmul  25173  dvmptcj  25177  dvmptco  25181  rolle  25199  dvlip  25202  dvlipcn  25203  dvle  25216  dvivthlem1  25217  dvivth  25219  dvfsumle  25230  dvfsumge  25231  dvmptrecl  25233  dvfsumlem2  25236  pserdv  25633  logtayl  25860  relogbf  25986  rlimcxp  26168  o1cxp  26169  gsummpt2co  31353  psgnfzto1stlem  31412  measdivcstALTV  32238  probfinmeasbALTV  32441  probmeasb  32442  dstrvprob  32483  cvmsss2  33281  sdclem2  35944  3factsumint1  40071  dmmzp  40592  dvcosax  43516  dvnprodlem3  43538  itgcoscmulx  43559  stoweidlem27  43617  dirkeritg  43692  fourierdlem16  43713  fourierdlem21  43718  fourierdlem22  43719  fourierdlem39  43736  fourierdlem57  43753  fourierdlem58  43754  fourierdlem60  43756  fourierdlem61  43757  fourierdlem73  43769  fourierdlem83  43779  subsaliuncllem  43945  0ome  44117  hoi2toco  44195  elbigofrcl  45954  itcoval0mpt  46070