Theorem dmmptg 6242

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 2761	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6240	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3472	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3100	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3445	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 237	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2815	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3077  {crab 3413  Vcvv 3451   ↦ cmpt 5186  dom cdm 5651

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 2733  ax-sep 5249  ax-pr 5391

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-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rab 3414  df-v 3453  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 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  rnmpt0f  6243  ovmpt3rabdm  7678  suppssov1  8207  suppssov2  8208  suppssfv  8212  iinon  8341  onoviun  8344  noinfep  9654  cantnfdm  9658  axcc2lem  10507  negfi  12259  ccatalpha  14733  swrd0  14801  o1lo1  15697  o1lo12  15698  lo1mptrcl  15782  o1mptrcl  15783  o1add2  15784  o1mul2  15785  o1sub2  15786  lo1add  15787  lo1mul  15788  o1dif  15790  rlimneg  15807  lo1le  15812  rlimno1  15814  o1fsum  15973  divsfval  17712  subdrgint  21053  iscnp2  23550  ptcnplem  23933  xkoinjcn  23999  fbasrn  24196  prdsdsf  24679  ressprdsds  24683  mbfmptcl  25950  mbfdm2  25951  dvmptresicc  26229  dvmptcl  26272  dvmptadd  26273  dvmptmul  26274  dvmptres2  26275  dvmptcmul  26277  dvmptcj  26281  dvmptco  26285  rolle  26303  dvlip  26306  dvlipcn  26307  dvle  26320  dvivthlem1  26321  dvivth  26323  dvfsumle  26334  dvfsumge  26335  dvmptrecl  26337  dvfsumlem2  26340  pserdv  26749  logtayl  26981  relogbf  27112  rlimcxp  27294  o1cxp  27295  gsummpt2co  33602  psgnfzto1stlem  33654  measdivcstALTV  34851  probfinmeasbALTV  35054  probmeasb  35055  dstrvprob  35097  cvmsss2  36018  sdclem2  38656  3factsumint1  43051  dmmzp  43723  dvcosax  46905  dvnprodlem3  46927  itgcoscmulx  46948  stoweidlem27  47006  dirkeritg  47081  fourierdlem16  47102  fourierdlem21  47107  fourierdlem22  47108  fourierdlem39  47125  fourierdlem57  47142  fourierdlem58  47143  fourierdlem60  47145  fourierdlem61  47146  fourierdlem73  47158  fourierdlem83  47168  subsaliuncllem  47336  0ome  47508  hoi2toco  47586  tmachlem-agreefin  47927  elbigofrcl  49631  itcoval0mpt  49747