Theorem dmmptg 6238

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 2760	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6236	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3471	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3444	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 237	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2814	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3076  {crab 3412  Vcvv 3450   ↦ cmpt 5186  dom cdm 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  rnmpt0f  6239  ovmpt3rabdm  7673  suppssov1  8195  suppssov2  8196  suppssfv  8200  iinon  8329  onoviun  8332  noinfep  9639  cantnfdm  9643  axcc2lem  10438  negfi  12188  ccatalpha  14660  swrd0  14728  o1lo1  15624  o1lo12  15625  lo1mptrcl  15709  o1mptrcl  15710  o1add2  15711  o1mul2  15712  o1sub2  15713  lo1add  15714  lo1mul  15715  o1dif  15717  rlimneg  15734  lo1le  15739  rlimno1  15741  o1fsum  15900  divsfval  17633  subdrgint  20969  iscnp2  23464  ptcnplem  23847  xkoinjcn  23913  fbasrn  24110  prdsdsf  24593  ressprdsds  24597  mbfmptcl  25864  mbfdm2  25865  dvmptresicc  26143  dvmptcl  26186  dvmptadd  26187  dvmptmul  26188  dvmptres2  26189  dvmptcmul  26191  dvmptcj  26195  dvmptco  26199  rolle  26217  dvlip  26220  dvlipcn  26221  dvle  26234  dvivthlem1  26235  dvivth  26237  dvfsumle  26248  dvfsumge  26249  dvmptrecl  26251  dvfsumlem2  26254  pserdv  26665  logtayl  26897  relogbf  27028  rlimcxp  27210  o1cxp  27211  gsummpt2co  33488  psgnfzto1stlem  33540  measdivcstALTV  34736  probfinmeasbALTV  34940  probmeasb  34941  dstrvprob  34983  cvmsss2  35853  sdclem2  38492  3factsumint1  42887  dmmzp  43578  dvcosax  46754  dvnprodlem3  46776  itgcoscmulx  46797  stoweidlem27  46855  dirkeritg  46930  fourierdlem16  46951  fourierdlem21  46956  fourierdlem22  46957  fourierdlem39  46974  fourierdlem57  46991  fourierdlem58  46992  fourierdlem60  46994  fourierdlem61  46995  fourierdlem73  47007  fourierdlem83  47017  subsaliuncllem  47185  0ome  47357  hoi2toco  47435  tmachlem-agreefin  47776  elbigofrcl  49480  itcoval0mpt  49596