Theorem dmmptg 6248

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 2725	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6246	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3480	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3072	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3452	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 233	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2784	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  ∀wral 3050  {crab 3418  Vcvv 3461   ↦ cmpt 5232  dom cdm 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-mpt 5233  df-xp 5684  df-rel 5685  df-cnv 5686  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691

This theorem is referenced by:  rnmpt0f  6249  ovmpt3rabdm  7680  suppssov1  8203  suppssov2  8204  suppssfv  8208  iinon  8361  onoviun  8364  noinfep  9690  cantnfdm  9694  axcc2lem  10466  negfi  12201  ccatalpha  14584  swrd0  14649  o1lo1  15522  o1lo12  15523  lo1mptrcl  15607  o1mptrcl  15608  o1add2  15609  o1mul2  15610  o1sub2  15611  lo1add  15612  lo1mul  15613  o1dif  15615  rlimneg  15634  lo1le  15639  rlimno1  15641  o1fsum  15800  divsfval  17537  subdrgint  20708  iscnp2  23192  ptcnplem  23574  xkoinjcn  23640  fbasrn  23837  prdsdsf  24322  ressprdsds  24326  mbfmptcl  25614  mbfdm2  25615  dvmptresicc  25894  dvmptcl  25940  dvmptadd  25941  dvmptmul  25942  dvmptres2  25943  dvmptcmul  25945  dvmptcj  25949  dvmptco  25953  rolle  25971  dvlip  25975  dvlipcn  25976  dvle  25989  dvivthlem1  25990  dvivth  25992  dvfsumle  26003  dvfsumleOLD  26004  dvfsumge  26005  dvmptrecl  26007  dvfsumlem2  26010  dvfsumlem2OLD  26011  pserdv  26416  logtayl  26644  relogbf  26773  rlimcxp  26956  o1cxp  26957  gsummpt2co  32857  psgnfzto1stlem  32918  measdivcstALTV  33977  probfinmeasbALTV  34182  probmeasb  34183  dstrvprob  34224  cvmsss2  35017  sdclem2  37348  3factsumint1  41626  dmmzp  42297  dvcosax  45454  dvnprodlem3  45476  itgcoscmulx  45497  stoweidlem27  45555  dirkeritg  45630  fourierdlem16  45651  fourierdlem21  45656  fourierdlem22  45657  fourierdlem39  45674  fourierdlem57  45691  fourierdlem58  45692  fourierdlem60  45694  fourierdlem61  45695  fourierdlem73  45707  fourierdlem83  45717  subsaliuncllem  45885  0ome  46057  hoi2toco  46135  elbigofrcl  47811  itcoval0mpt  47927