Theorem dmmptg 6208

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 2737	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6206	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3463	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3434	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2791	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {crab 3401  Vcvv 3442   ↦ cmpt 5181  dom cdm 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-xp 5638  df-rel 5639  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  rnmpt0f  6209  ovmpt3rabdm  7627  suppssov1  8149  suppssov2  8150  suppssfv  8154  iinon  8282  onoviun  8285  noinfep  9581  cantnfdm  9585  axcc2lem  10358  negfi  12103  ccatalpha  14529  swrd0  14594  o1lo1  15472  o1lo12  15473  lo1mptrcl  15557  o1mptrcl  15558  o1add2  15559  o1mul2  15560  o1sub2  15561  lo1add  15562  lo1mul  15563  o1dif  15565  rlimneg  15582  lo1le  15587  rlimno1  15589  o1fsum  15748  divsfval  17480  subdrgint  20748  iscnp2  23195  ptcnplem  23577  xkoinjcn  23643  fbasrn  23840  prdsdsf  24323  ressprdsds  24327  mbfmptcl  25605  mbfdm2  25606  dvmptresicc  25885  dvmptcl  25931  dvmptadd  25932  dvmptmul  25933  dvmptres2  25934  dvmptcmul  25936  dvmptcj  25940  dvmptco  25944  rolle  25962  dvlip  25966  dvlipcn  25967  dvle  25980  dvivthlem1  25981  dvivth  25983  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvmptrecl  25998  dvfsumlem2  26001  dvfsumlem2OLD  26002  pserdv  26407  logtayl  26637  relogbf  26769  rlimcxp  26952  o1cxp  26953  gsummpt2co  33142  psgnfzto1stlem  33194  measdivcstALTV  34403  probfinmeasbALTV  34607  probmeasb  34608  dstrvprob  34650  cvmsss2  35490  sdclem2  37993  3factsumint1  42391  dmmzp  43090  dvcosax  46284  dvnprodlem3  46306  itgcoscmulx  46327  stoweidlem27  46385  dirkeritg  46460  fourierdlem16  46481  fourierdlem21  46486  fourierdlem22  46487  fourierdlem39  46504  fourierdlem57  46521  fourierdlem58  46522  fourierdlem60  46524  fourierdlem61  46525  fourierdlem73  46537  fourierdlem83  46547  subsaliuncllem  46715  0ome  46887  hoi2toco  46965  elbigofrcl  48910  itcoval0mpt  49026