Theorem dmmptg 6245

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 6243	. 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 1569   ∈ wcel 2144  ∀wral 3076  {crab 3412  Vcvv 3450   ↦ cmpt 5185  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  rnmpt0f  6246  ovmpt3rabdm  7682  suppssov1  8219  suppssov2  8220  suppssfv  8224  iinon  8353  onoviun  8356  noinfep  9666  cantnfdm  9670  axcc2lem  10519  negfi  12271  ccatalpha  14745  swrd0  14814  o1lo1  15711  o1lo12  15712  lo1mptrcl  15796  o1mptrcl  15797  o1add2  15798  o1mul2  15799  o1sub2  15800  lo1add  15801  lo1mul  15802  o1dif  15804  rlimneg  15821  lo1le  15826  rlimno1  15828  o1fsum  15987  divsfval  17726  subdrgint  21067  iscnp2  23564  ptcnplem  23947  xkoinjcn  24013  fbasrn  24210  prdsdsf  24693  ressprdsds  24697  mbfmptcl  25964  mbfdm2  25965  dvmptresicc  26243  dvmptcl  26286  dvmptadd  26287  dvmptmul  26288  dvmptres2  26289  dvmptcmul  26291  dvmptcj  26295  dvmptco  26299  rolle  26317  dvlip  26320  dvlipcn  26321  dvle  26334  dvivthlem1  26335  dvivth  26337  dvfsumle  26348  dvfsumge  26349  dvmptrecl  26351  dvfsumlem2  26354  pserdv  26763  logtayl  26995  relogbf  27126  rlimcxp  27308  o1cxp  27309  gsummpt2co  33657  psgnfzto1stlem  33709  measdivcstALTV  34906  probfinmeasbALTV  35109  probmeasb  35110  dstrvprob  35152  cvmsss2  36127  sdclem2  38783  3factsumint1  43178  dmmzp  43851  dvcosax  47043  dvnprodlem3  47065  itgcoscmulx  47086  stoweidlem27  47144  dirkeritg  47219  fourierdlem16  47240  fourierdlem21  47245  fourierdlem22  47246  fourierdlem39  47263  fourierdlem57  47280  fourierdlem58  47281  fourierdlem60  47283  fourierdlem61  47284  fourierdlem73  47296  fourierdlem83  47306  subsaliuncllem  47474  0ome  47646  hoi2toco  47724  tmachlem-agreefin  48065  elbigofrcl  49769  itcoval0mpt  49885