Theorem dmmptg 6197

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 2733	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	dmmpt 6195	. 2 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}
3		elex 3458	. . . 4 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V)
4	3	ralimi 3070	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
5		rabid2 3429	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V)
6	4, 5	sylibr 234	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V})
7	2, 6	eqtr4id 2787	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3048  {crab 3396  Vcvv 3437   ↦ cmpt 5176  dom cdm 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-mpt 5177  df-xp 5627  df-rel 5628  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634

This theorem is referenced by:  rnmpt0f  6198  ovmpt3rabdm  7614  suppssov1  8136  suppssov2  8137  suppssfv  8141  iinon  8269  onoviun  8272  noinfep  9561  cantnfdm  9565  axcc2lem  10338  negfi  12082  ccatalpha  14508  swrd0  14573  o1lo1  15451  o1lo12  15452  lo1mptrcl  15536  o1mptrcl  15537  o1add2  15538  o1mul2  15539  o1sub2  15540  lo1add  15541  lo1mul  15542  o1dif  15544  rlimneg  15561  lo1le  15566  rlimno1  15568  o1fsum  15727  divsfval  17459  subdrgint  20727  iscnp2  23174  ptcnplem  23556  xkoinjcn  23622  fbasrn  23819  prdsdsf  24302  ressprdsds  24306  mbfmptcl  25584  mbfdm2  25585  dvmptresicc  25864  dvmptcl  25910  dvmptadd  25911  dvmptmul  25912  dvmptres2  25913  dvmptcmul  25915  dvmptcj  25919  dvmptco  25923  rolle  25941  dvlip  25945  dvlipcn  25946  dvle  25959  dvivthlem1  25960  dvivth  25962  dvfsumle  25973  dvfsumleOLD  25974  dvfsumge  25975  dvmptrecl  25977  dvfsumlem2  25980  dvfsumlem2OLD  25981  pserdv  26386  logtayl  26616  relogbf  26748  rlimcxp  26931  o1cxp  26932  gsummpt2co  33059  psgnfzto1stlem  33110  measdivcstALTV  34310  probfinmeasbALTV  34514  probmeasb  34515  dstrvprob  34557  cvmsss2  35390  sdclem2  37855  3factsumint1  42187  dmmzp  42890  dvcosax  46086  dvnprodlem3  46108  itgcoscmulx  46129  stoweidlem27  46187  dirkeritg  46262  fourierdlem16  46283  fourierdlem21  46288  fourierdlem22  46289  fourierdlem39  46306  fourierdlem57  46323  fourierdlem58  46324  fourierdlem60  46326  fourierdlem61  46327  fourierdlem73  46339  fourierdlem83  46349  subsaliuncllem  46517  0ome  46689  hoi2toco  46767  elbigofrcl  48712  itcoval0mpt  48828